A finite product of weighted measures is the product measure with the product weight

MeasureTheory.Measure.pi (fun i => (μ i).withDensity (f i)) is (MeasureTheory.Measure.pi μ).withDensity (fun x => ∏ i, f i (x i)): putting a density on each factor of a finite product measure is the same as putting the product of the densities on the product measure.

Mathlib has the two-factor versions MeasureTheory.Measure.prod_withDensity₀ and MeasureTheory.Measure.prod_withDensity but not the MeasureTheory.Measure.pi version, which is what a coordinatewise weight on ℝ^ι needs. The motivating instance is the multivariate Gaussian, whose product measure is Lebesgue measure on ℝ^ι weighted by the product of the one-dimensional Gaussian densities.

The proof identifies the two measures on measurable boxes via MeasureTheory.Measure.pi_eq; the box computation is TauCeti.lintegral_fintype_prod_eq_prod₀ applied to the indicator-truncated densities.

Main statements

• TauCeti.pi_withDensity₀: the identification, for almost everywhere measurable densities.
• TauCeti.pi_withDensity: the same for measurable densities.

theorem TauCeti.pi_withDensity₀ {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)} (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {f : (i : ι) → α i → ENNReal} (hf : ∀ (i : ι), AEMeasurable (f i) (μ i)) [∀ (i : ι), MeasureTheory.SigmaFinite ((μ i).withDensity (f i))] : (MeasureTheory.Measure.pi fun (i : ι) => (μ i).withDensity (f i)) = (MeasureTheory.Measure.pi μ).withDensity fun (x : (i : ι) → α i) => ∏ i : ι, f i (x i)

Coordinatewise densities multiply. For a finite family of σ-finite measures μ i and almost everywhere measurable densities f i, the product of the weighted measures (μ i).withDensity (f i) is the product measure weighted by the product density x ↦ ∏ i, f i (x i).

The σ-finiteness assumption on the weighted factors is what MeasureTheory.Measure.pi_eq needs to recognize the left-hand side as the product measure; it is automatic when the weighted factors are finite (as for probability densities).

theorem TauCeti.pi_withDensity {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)} (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {f : (i : ι) → α i → ENNReal} (hf : ∀ (i : ι), Measurable (f i)) [∀ (i : ι), MeasureTheory.SigmaFinite ((μ i).withDensity (f i))] : (MeasureTheory.Measure.pi fun (i : ι) => (μ i).withDensity (f i)) = (MeasureTheory.Measure.pi μ).withDensity fun (x : (i : ι) → α i) => ∏ i : ι, f i (x i)

Coordinatewise densities multiply, for measurable densities; see TauCeti.pi_withDensity₀ for the almost everywhere measurable version.