map_apply' — Mathlib

English

For a probability measure ν and aemeasurable function f, the pushforward ν.map f equals the measure induced by f on the σ-algebra, i.e., (ν.map f) A = ν(f^{-1}(A)).

Русский

Для вероятностной меры ν и функции f, измеряемой относительно ν, образная мера ν.map f задаёт (ν.map f)(A) = ν(f^{-1}(A)).

LaTeX

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

Lean4

/-- Note that this is an equality of elements of `ℝ≥0∞`. See also
`MeasureTheory.ProbabilityMeasure.map_apply` for the corresponding equality as elements of `ℝ≥0`. -/
theorem map_apply' (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) {A : Set Ω'}
    (A_mble : MeasurableSet A) : (ν.map f_aemble : Measure Ω') A = (ν : Measure Ω) (f ⁻¹' A) :=
  Measure.map_apply_of_aemeasurable f_aemble A_mble

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