measurePreserving_piCongrLeft — Mathlib

English

The pi-congruence left permutation preserves the measure after rearranging indices by an equivalence f.

Русский

Похождение слева через конгруентность(piCongrLeft) сохраняет меру после перестановки индексов по эквивалентности f.

LaTeX

$$$MeasurePreserving(\mathrm{piCongrLeft}(\alpha,f))(Measure.pi(\mu)) = Measure.pi(\mu \circ f)$$$

Lean4

theorem measurePreserving_piCongrLeft (f : ι' ≃ ι) :
    MeasurePreserving (MeasurableEquiv.piCongrLeft α f) (Measure.pi fun i' => μ (f i')) (Measure.pi μ)
    where
  measurable := (MeasurableEquiv.piCongrLeft α f).measurable
  map_eq := by
    refine (pi_eq fun s _ => ?_).symm
    rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_piCongrLeft f, Equiv.piCongrLeft_preimage_univ_pi, pi_pi _ _,
      f.prod_comp (fun i => μ i (s i))]

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