map_apply_of_aemeasurable — Mathlib

English

Equivalent pushforward equality for measurable sets: (ν.map f_aemble) A = ν (f^{-1} A).

Русский

Эквивалентность образующей меры на множество: (ν.map f_aemble) A = ν(f^{-1} A).

LaTeX

$$$ (ν.map f_{aemble}) A = ν (f^{-1} A) $$$

Lean4

theorem map_apply_of_aemeasurable (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) {A : Set Ω'}
    (A_mble : MeasurableSet A) : (ν.map f_aemble) A = ν (f ⁻¹' A) := by
  exact
    (ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr <| ν.map_apply' f_aemble A_mble

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