map_apply_of_aemeasurable — Mathlib

English

A specialization of the previous law for a general measurable f without AEMEAS assumptions when f is measured with ν.toMeasure.

Русский

Специализация правила переноса меры: применимо без дополнительных предположений к измеримой f.

LaTeX

$$$ν.map f(A) = ν(f^{-1}(A))$ for Measurable f and Measurable A$$

Lean4

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

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