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