Mathlib upstream candidate: Tonelli for a product over a finite index (lintegral)

The lintegral (ℝ≥0∞-valued) analogue of MeasureTheory.integral_fintype_prod_eq_prod: on a finite product of σ-finite measure spaces, the lower integral of a product of single-coordinate functions is the product of the lower integrals,

∫⁻ x, ∏ i, f i (x i) ∂(Measure.pi μ) = ∏ i, ∫⁻ x, f i x ∂(μ i).

Mathlib has the Bochner version (Integral/Pi.lean) but no lintegral form. The proof mirrors the Bochner one: induct on Fin n via measurePreserving_piFinSuccAbove

• lintegral_prod_mul, then transfer to a general finite index by equivFin + measurePreserving_piCongrLeft.

Category: 1-Mathlib (CSD-free; staged as a Mathlib upstream candidate).

Provenance

Needed for the general-N Duistermaat–Heckman / Dirichlet computation (CsdLean4/LF4/MomentRatioUniformN.lean, Slice D.5): the joint Exp(1/2)^{⊗N} density is a product of single-coordinate densities, and exposing it requires this lower-integral Fubini fact (and the pi-withDensity bridge built on it). See specs/general-n-dh-plan.md Slice D.5a.

Tags

lintegral, Fubini, Tonelli, product measure, pi

theorem MeasureTheory.lintegral_fin_nat_prod_eq_prod {n : ℕ} {E : Fin n → Type u_2} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)} [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → ENNReal) (hf : ∀ (i : Fin n), Measurable (f i)) : ∫⁻ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi μ = ∏ i : Fin n, ∫⁻ (x : E i), f i x ∂μ i

Tonelli for a product over Fin n (lintegral). The lower integral of a product of single-coordinate functions over Measure.pi is the product of the lower integrals. Proved by induction on n (measurePreserving_piFinSuccAbove splits off the 0-th coordinate; lintegral_prod_mul factors the resulting product).

theorem MeasureTheory.lintegral_fintype_prod_eq_prod {ι : Type u_1} [Fintype ι] {E : ι → Type u_2} {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → Measure (E i)} [∀ (i : ι), SigmaFinite (μ i)] (f : (i : ι) → E i → ENNReal) (hf : ∀ (i : ι), Measurable (f i)) : ∫⁻ (x : (i : ι) → E i), ∏ i : ι, f i (x i) ∂Measure.pi μ = ∏ i : ι, ∫⁻ (x : E i), f i x ∂μ i

Tonelli for a product over a finite index (lintegral). The general-index version, transferred from lintegral_fin_nat_prod_eq_prod via equivFin.

theorem MeasureTheory.pi_withDensity {ι : Type u_1} [Fintype ι] {E : ι → Type u_2} {mE : (i : ι) → MeasurableSpace (E i)} (μ : (i : ι) → Measure (E i)) [∀ (i : ι), SigmaFinite (μ i)] (g : (i : ι) → E i → ENNReal) (hg : ∀ (i : ι), Measurable (g i)) [∀ (i : ι), SigmaFinite ((μ i).withDensity (g i))] : (Measure.pi fun (i : ι) => (μ i).withDensity (g i)) = (Measure.pi μ).withDensity fun (x : (i : ι) → E i) => ∏ i : ι, g i (x i)

The pi-withDensity bridge. A finite product of measures, each given a density, is the product measure with the product density: Measure.pi (fun i => (μ i).withDensity (g i)) = (Measure.pi μ).withDensity (fun x => ∏ i, g i (x i)). The pi analogue of MeasureTheory.prod_withDensity. Proved by Measure.pi_eq on rectangles, using lintegral_fintype_prod_eq_prod (D.5a) to factor the product-density integral over the rectangle.