English
Consider a two-indexed family α: Fin 2 → Type and measurable spaces on each α i. The canonical piFinTwo equivalence between the two-factor product and the product measure (μ0 × μ1) is measure-preserving.
Русский
У рассмотримого семейства с двумя индексами α: Fin 2 → Type, для каждого i задано пространство меры. Каноническое отображение piFinTwo между произведением двух факторов и произведением мер сохраняет меру.
LaTeX
$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.piFinTwo}(\alpha)\bigr) \, (\mathrm{Measure.pi}\, μ) \, (μ_0 \times μ_1) $$$
Lean4
theorem measurePreserving_piFinTwo {α : Fin 2 → Type u} {m : ∀ i, MeasurableSpace (α i)} (μ : ∀ i, Measure (α i))
[∀ i, SigmaFinite (μ i)] : MeasurePreserving (MeasurableEquiv.piFinTwo α) (Measure.pi μ) ((μ 0).prod (μ 1)) :=
by
refine ⟨MeasurableEquiv.measurable _, (Measure.prod_eq fun s t _ _ => ?_).symm⟩
rw [MeasurableEquiv.map_apply, MeasurableEquiv.piFinTwo_apply, Fin.preimage_apply_01_prod, Measure.pi_pi,
Fin.prod_univ_two]
rfl
