toMeasure_map_apply — Mathlib

English

For a PMF p and measurable f, the pushforward measure of p via map f equals the measure obtained by mapping p via f.

Русский

Пусть p — PMF и f измеримая; образ via map f совпадает с мерой, полученной отображением p через f.

LaTeX

$$$ (p.map f).toMeasure s = p.toMeasure (f^{-1}'s s) $$$

Lean4

@[simp]
theorem toMeasure_map_apply (hf : Measurable f) (hs : MeasurableSet s) :
    (p.map f).toMeasure s = p.toMeasure (f ⁻¹' s) :=
  by
  rw [toMeasure_apply_eq_toOuterMeasure_apply _ hs,
    toMeasure_apply_eq_toOuterMeasure_apply _ (measurableSet_preimage hf hs)]
  exact toOuterMeasure_map_apply f p s

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