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.
• TauCeti.integral_pi_sum_mul: Fubini over a sum of index types, for a product of a function of each block of coordinates.

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.

theorem TauCeti.integral_pi_sum_mul {ι : Type u_3} {ι' : Type u_4} [Fintype ι] [Fintype ι'] {α : ι ⊕ ι' → Type u_5} [(i : ι ⊕ ι') → MeasurableSpace (α i)] (μ : (i : ι ⊕ ι') → MeasureTheory.Measure (α i)) [∀ (i : ι ⊕ ι'), MeasureTheory.SigmaFinite (μ i)] {L : Type u_6} [RCLike L] (f : ((i : ι) → α (Sum.inl i)) → L) (g : ((i : ι') → α (Sum.inr i)) → L) : ∫ (x : (i : ι ⊕ ι') → α i), (f fun (i : ι) => x (Sum.inl i)) * g fun (i : ι') => x (Sum.inr i) ∂MeasureTheory.Measure.pi μ = (∫ (y : (i : ι) → α (Sum.inl i)), f y ∂MeasureTheory.Measure.pi fun (i : ι) => μ (Sum.inl i)) * ∫ (y : (i : ι') → α (Sum.inr i)), g y ∂MeasureTheory.Measure.pi fun (i : ι') => μ (Sum.inr i)

Fubini over a sum of index types. Over a finite product measure indexed by ι ⊕ ι', the integral of a function of the ι coordinates times a function of the ι' coordinates is the product of the two integrals.