Marginals of multivariate functions #
In this file, we define a convenient way to compute integrals of multivariate functions, especially
if you want to write expressions where you integrate only over some of the variables that the
function depends on. This is common in induction arguments involving integrals of multivariate
functions.
This constructions allows working with iterated integrals and applying Tonelli's theorem
and Fubini's theorem, without using measurable equivalences by changing the representation of your
space (e.g. ((ι ⊕ ι') → ℝ) ≃ (ι → ℝ) × (ι' → ℝ)).
Main Definitions #
- Assume that
∀ i : ι, π iis a product of measurable spaces with measuresμ ionπ i,f : (∀ i, π i) → ℝ≥0∞is a function ands : Finset ι. Thenlmarginal μ s for∫⋯∫⁻_s, f ∂μis the function that integratesfover all variables ins. It returns a function that still takes the same variables asf, but is constant in the variables ins. Mathematically, ifs = {i₁, ..., iₖ}, thenlmarginal μ s fis the expression $$ \vec{x}\mapsto \int\!\!\cdots\!\!\int f(\vec{x}[\vec{y}])dy_{i_1}\cdots dy_{i_k}. $$ where $\vec{x}[\vec{y}]$ is the vector $\vec{x}$ with $x_{i_j}$ replaced by $y_{i_j}$ for all $1 \le j \le k$. Iffis the distribution of a random variable, this is the marginal distribution of all variables not ins(but not the most general notion, since we only consider product measures here). Note that the notation∫⋯∫⁻_s, f ∂μis not a binder, and returns a function.
Main Results #
lmarginal_unionis the analogue of Tonelli's theorem for iterated integrals. It states that for measurable functionsfand disjoint finsetssandtwe have∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ.
Implementation notes #
The function f can have an arbitrary product as its domain (even infinite products), but the
set s of integration variables is a Finset. We are assuming that the function f is measurable
for most of this file. Note that asking whether it is AEMeasurable is not even well-posed,
since there is no well-behaved measure on the domain of f.
TODO #
- Define the marginal function for functions taking values in a Banach space.
Integrate f(x₁,…,xₙ) over all variables xᵢ where i ∈ s. Return a function in the
remaining variables (it will be constant in the xᵢ for i ∈ s).
This is the marginal distribution of all variables not in s when the considered measure
is the product measure.
Equations
- (∫⋯∫⁻_s, f ∂μ) x = ∫⁻ (y : (i : { x : δ // x ∈ s }) → π ↑i), f (Function.updateFinset x s y) ∂MeasureTheory.Measure.pi fun (i : { x : δ // x ∈ s }) => μ ↑i
Instances For
Integrate f(x₁,…,xₙ) over all variables xᵢ where i ∈ s. Return a function in the
remaining variables (it will be constant in the xᵢ for i ∈ s).
This is the marginal distribution of all variables not in s when the considered measure
is the product measure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Integrate f(x₁,…,xₙ) over all variables xᵢ where i ∈ s. Return a function in the
remaining variables (it will be constant in the xᵢ for i ∈ s).
This is the marginal distribution of all variables not in s when the considered measure
is the product measure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The marginal distribution is independent of the variables in s.
Peel off a single integral from a lmarginal integral at the beginning (compare with
lmarginal_insert', which peels off an integral at the end).
Peel off a single integral from a lmarginal integral at the beginning (compare with
lmarginal_erase', which peels off an integral at the end).
Peel off a single integral from a lmarginal integral at the end (compare with
lmarginal_insert, which peels off an integral at the beginning).
Peel off a single integral from a lmarginal integral at the end (compare with
lmarginal_erase, which peels off an integral at the beginning).