Marginal integrals of products

For a product measure ∏ i, μ i on ∀ i, X i and a finite set s of coordinates, the marginal integral ∫⋯∫⁻_s, f ∂μ of Mathlib is the integral of f over the coordinates in s, which is a function of the other coordinates. Three rules are proved here, by which the densities of the forward passes of the paper are integrated:

• a factor which does not depend on the coordinates in s comes out of the marginal integral over s (lmarginal_mul_left);
• the marginal integral over s of a product of factors, each of which depends on a single coordinate in s and on the coordinates outside s, is the product of the marginal integrals of the factors over their coordinates (lmarginal_prod);
• the integral over the coordinates outside s of the marginal integral over s, with the coordinates outside s inserted by a map g, is the integral over all the coordinates (lintegral_lmarginal_comp). For the forward passes, these coordinates are those of the reference trajectory.

Dependence on a set of coordinates is expressed by Mathlib's DependsOn.

theorem CSMC.dependsOn_lmarginal {δ : Type u_1} {X : δ → Type u_3} [(i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)} [DecidableEq δ] {f : ((i : δ) → X i) → ENNReal} {u : Set δ} (hf : DependsOn f u) (s : Finset δ) : DependsOn (∫⋯∫⁻_s, f ∂μ) (u \ ↑s)

If f depends only on the coordinates in u, its marginal integral over s depends only on the coordinates in u \ s.

theorem CSMC.lmarginal_mul_left {δ : Type u_1} {X : δ → Type u_3} [(i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)} [DecidableEq δ] {s : Finset δ} {f g : ((i : δ) → X i) → ENNReal} (hf : Measurable f) (hg : DependsOn g (↑s)ᶜ) (x : (i : δ) → X i) : (∫⋯∫⁻_s, fun (y : (i : δ) → X i) => g y * f y ∂μ) x = g x * (∫⋯∫⁻_s, f ∂μ) x

A factor which does not depend on the coordinates in s comes out of the marginal integral over s.

theorem CSMC.lmarginal_prod {δ : Type u_1} {X : δ → Type u_3} [(i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)} [DecidableEq δ] [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] {s : Finset δ} {g : δ → ((i : δ) → X i) → ENNReal} (hg : ∀ i ∈ s, Measurable (g i)) (hdep : ∀ i ∈ s, DependsOn (g i) (insert i (↑s)ᶜ)) (x : (i : δ) → X i) : (∫⋯∫⁻_s, fun (y : (i : δ) → X i) => ∏ i ∈ s, g i y ∂μ) x = ∏ i ∈ s, (∫⋯∫⁻_{i}, g i ∂μ) x

The marginal integral over s of a product of factors g i, i ∈ s, each of which depends only on the coordinate i and on the coordinates outside s, is the product of the marginal integrals of the factors g i over the coordinate i.

theorem CSMC.lintegral_lmarginal_comp {δ : Type u_1} {δ' : Type u_2} {X : δ → Type u_3} [(i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)} [DecidableEq δ] [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [Fintype δ] [Fintype δ'] {s : Finset δ} {e : δ' → δ} (he : Function.Injective e) (hs : ∀ (i : δ), i ∉ s ↔ i ∈ Set.range e) {g : ((j : δ') → X (e j)) → (i : δ) → X i} (hg : Measurable g) (hge : ∀ (x : (j : δ') → X (e j)) (j : δ'), g x (e j) = x j) {f : ((i : δ) → X i) → ENNReal} (hf : Measurable f) : (∫⁻ (x : (i : δ') → X (e i)), (∫⋯∫⁻_s, f ∂μ) (g x) ∂MeasureTheory.Measure.pi fun (j : δ') => μ (e j)) = ∫⁻ (y : (i : δ) → X i), f y ∂MeasureTheory.Measure.pi μ

Let g insert a point of ∀ j, X (e j) at the coordinates e j, which are the coordinates outside s. The integral over these coordinates of the marginal integral over s, evaluated at the point inserted by g, is the integral over all the coordinates.