Integrals over finite product measures

This file collects integration results for finite product measures. In addition to the lower integral product formula, it gives a Fubini identity obtained by refreshing two coordinates with independent samples.

The ℝ≥0∞-valued companion of Mathlib's MeasureTheory.integral_fintype_prod_eq_prod: over MeasureTheory.Measure.pi, the lower integral of a product ∏ i, f i (x i) of functions each depending on a single coordinate is the product of the one-dimensional lower integrals.

Mathlib proves the Bochner version (and the matching integrability statements) but not this one, even though the ℝ≥0∞ version needs no integrability hypothesis at all, since every factor is automatically "integrable" in the lower-integral sense. The proof is the same induction as Mathlib's: reduce a Fin (n + 1)-indexed product to a binary product measure along MeasureTheory.measurePreserving_piFinSuccAbove, split it with MeasureTheory.lintegral_prod_mul, and transfer an arbitrary Fintype index to Fin along MeasureTheory.measurePreserving_piCongrLeft.

Main statements

• TauCeti.lintegral_fintype_prod_eq_prod: the product formula, for measurable factors.
• TauCeti.lintegral_fintype_prod_eq_prod₀: the same for almost everywhere measurable factors.
• TauCeti.integral_pi_eq_integral_integral_update: the two-coordinate Fubini identity.

theorem TauCeti.integral_pi_eq_integral_integral_update {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {a b : ι} [MeasureTheory.IsProbabilityMeasure (μ a)] [MeasureTheory.IsProbabilityMeasure (μ b)] (hab : a ≠ b) {f : ((i : ι) → α i) → E} (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi μ)) : ∫ (x : (i : ι) → α i), f x ∂MeasureTheory.Measure.pi μ = ∫ (z : (i : ι) → α i), ∫ (p : α a × α b), f (Function.update (Function.update z a p.1) b p.2) ∂(μ a).prod (μ b) ∂MeasureTheory.Measure.pi μ

Fubini after a two-coordinate refresh. An integral against a finite product of sigma-finite measures is an outer integral over the assignment and an inner integral over a fresh independent pair placed at the two distinct probability coordinates a and b.

theorem TauCeti.lintegral_fintype_prod_eq_prod {ι : Type u_3} [Fintype ι] {α : ι → Type u_4} {mα : (i : ι) → MeasurableSpace (α i)} (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {f : (i : ι) → α i → ENNReal} (hf : ∀ (i : ι), Measurable (f i)) : ∫⁻ (x : (i : ι) → α i), ∏ i : ι, f i (x i) ∂MeasureTheory.Measure.pi μ = ∏ i : ι, ∫⁻ (y : α i), f i y ∂μ i

The product formula for lower integrals over a finite product measure. The lower integral of ∏ i, f i (x i) against MeasureTheory.Measure.pi μ is ∏ i, ∫⁻ y, f i y ∂μ i.

This is the ℝ≥0∞ analogue of MeasureTheory.integral_fintype_prod_eq_prod; unlike the Bochner statement it needs no integrability of the factors. See TauCeti.lintegral_fintype_prod_eq_prod₀ for the almost everywhere measurable version, which is obtained from this one by passing to measurable representatives.

theorem TauCeti.lintegral_fintype_prod_eq_prod₀ {ι : Type u_3} [Fintype ι] {α : ι → Type u_4} {mα : (i : ι) → MeasurableSpace (α i)} (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {f : (i : ι) → α i → ENNReal} (hf : ∀ (i : ι), AEMeasurable (f i) (μ i)) : ∫⁻ (x : (i : ι) → α i), ∏ i : ι, f i (x i) ∂MeasureTheory.Measure.pi μ = ∏ i : ι, ∫⁻ (y : α i), f i y ∂μ i

The product formula for lower integrals over a finite product measure, for almost everywhere measurable factors; see TauCeti.lintegral_fintype_prod_eq_prod for the measurable version.