measurePreserving_piFinSuccAbove — Mathlib

English

The symmetric version of preservation of measure for the sum-Pi to Pi-Prod-Pi equivalence.

Русский

Симметрическая версия сохранения меры для эквивалентности sumPi и PiProdPi.

LaTeX

$$measurePreserving_sumPiEquivProdPi_symm (X) :$$

Lean4

theorem measurePreserving_piFinSuccAbove {n : ℕ} {α : Fin (n + 1) → Type u} {m : ∀ i, MeasurableSpace (α i)}
    (μ : ∀ i, Measure (α i)) [∀ i, SigmaFinite (μ i)] (i : Fin (n + 1)) :
    MeasurePreserving (MeasurableEquiv.piFinSuccAbove α i) (Measure.pi μ)
      ((μ i).prod <| Measure.pi fun j => μ (i.succAbove j)) :=
  by
  set e := (MeasurableEquiv.piFinSuccAbove α i).symm
  refine MeasurePreserving.symm e ?_
  refine ⟨e.measurable, (pi_eq fun s _ => ?_).symm⟩
  rw [e.map_apply, i.prod_univ_succAbove _, ← pi_pi, ← prod_prod]
  congr 1 with ⟨x, f⟩
  simp [e, i.forall_iff_succAbove]

Похожие утверждения