English
If each index i carries a measure μ_i, and each μ_i is Sigma-finite, then the Pi-preserving map preserves measure between the Pi-space and the product space.
Русский
Если для каждого индекса i имеется мера μ_i, каждая из которых сигма-конечна, то сохраняется мера между Pi-пространством и произведением.
LaTeX
$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{fun\ i}\mapsto f_i\bigr)\; (\mathrm{Measure.pi}\mu)\; (\mathrm{Measure.pi}\nu) $$$
Lean4
/-- The measurable equiv `(α₁ → β₁) ≃ᵐ (α₂ → β₂)` induced by `α₁ ≃ α₂` and `β₁ ≃ᵐ β₂` is
measure preserving. -/
theorem measurePreserving_arrowCongr' {α₁ β₁ α₂ β₂ : Type*} [Fintype α₁] [Fintype α₂] [MeasurableSpace β₁]
[MeasurableSpace β₂] (μ : α₁ → Measure β₁) (ν : α₂ → Measure β₂) [∀ i, SigmaFinite (ν i)] (eα : α₁ ≃ α₂)
(eβ : β₁ ≃ᵐ β₂) (hm : ∀ i, MeasurePreserving eβ (μ i) (ν (eα i))) :
MeasurePreserving (MeasurableEquiv.arrowCongr' eα eβ) (Measure.pi fun i ↦ μ i) (Measure.pi fun i ↦ ν i) := by
classical
convert (measurePreserving_piCongrLeft (fun i : α₂ ↦ ν i) eα).comp (measurePreserving_pi μ (fun i : α₁ ↦ ν (eα i)) hm)
simp only [MeasurableEquiv.arrowCongr', Equiv.arrowCongr', Equiv.arrowCongr, EquivLike.coe_coe, comp_def,
MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, MeasurableEquiv.piCongrLeft, Equiv.piCongrLeft, Equiv.symm_symm,
Equiv.piCongrLeft', eq_rec_constant, Equiv.coe_fn_symm_mk]
