English
The canonical associativity isomorphism between triple product measures preserves measure.
Русский
Каноническое ассоциативное отображение между тройками произведений мер сохраняет меру.
LaTeX
$$MeasurePreserving( prodAssoc : ((α × β) × γ) ≃ᵐ (α × (β × γ)), ((μ_a.prod μ_b).prod μ_c), (μ_a.prod (μ_b.prod μ_c)))$$
Lean4
/-- The measurable equiv induced by the equiv `(α × β) × γ ≃ α × (β × γ)` is measure preserving. -/
theorem _root_.MeasureTheory.measurePreserving_prodAssoc (μa : Measure α) (μb : Measure β) (μc : Measure γ) [SFinite μb]
[SFinite μc] :
MeasurePreserving (MeasurableEquiv.prodAssoc : (α × β) × γ ≃ᵐ α × β × γ) ((μa.prod μb).prod μc)
(μa.prod (μb.prod μc))
where
measurable := MeasurableEquiv.prodAssoc.measurable
map_eq := by
ext s hs
have A (x : α) : MeasurableSet (Prod.mk x ⁻¹' s) := measurable_prodMk_left hs
have B : MeasurableSet (MeasurableEquiv.prodAssoc ⁻¹' s) := MeasurableEquiv.prodAssoc.measurable hs
simp_rw [map_apply MeasurableEquiv.prodAssoc.measurable hs, prod_apply hs, prod_apply (A _), prod_apply B,
lintegral_prod _ (measurable_measure_prodMk_left B).aemeasurable]
rfl
