English
If α ≃ α' and β ≃ᵐ β' are equivalences of types with measure spaces, the induced arrowCongr' map on function spaces is measure-preserving between the corresponding product measures.
Русский
Если есть эквивалентности между α и α' и между β и β', то индуцированное отображение стрелка-конгру на пространствах функций сохраняет меру между соответствующими произведениями мер.
LaTeX
$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.arrowCongr'}(eα,eβ)\bigr)\; (\mathrm{Measure.pi}\mu)\; (\mathrm{Measure.pi}\nu) $$$
Lean4
theorem measurePreserving_pi {ι : Type*} [Fintype ι] {α : ι → Type v} {β : ι → Type*} [∀ i, MeasurableSpace (α i)]
[∀ i, MeasurableSpace (β i)] (μ : (i : ι) → Measure (α i)) (ν : (i : ι) → Measure (β i))
{f : (i : ι) → (α i) → (β i)} [hν : ∀ i, SigmaFinite (ν i)] (hf : ∀ i, MeasurePreserving (f i) (μ i) (ν i)) :
MeasurePreserving (fun a i ↦ f i (a i)) (Measure.pi μ) (Measure.pi ν)
where
measurable := measurable_pi_iff.mpr <| fun i ↦ (hf i).measurable.comp (measurable_pi_apply i)
map_eq := by
have (i : ι) : SigmaFinite ((μ i).map (f i)) := (hf i).map_eq ▸ hν i
rw [pi_map_pi (fun i ↦ (hf i).aemeasurable)]
exact congrArg _ <| funext fun i ↦ (hf i).map_eq
