isProbabilityMeasure_map_iff — Mathlib

English

For an a.e.-measurable map f, IsProbabilityMeasure(μ.map f μ) is equivalent to IsProbabilityMeasure μ.

Русский

Для а.е.-изображения f равенство вероятностной меры μ.map f μ эквивалентно IsProbabilityMeasure μ.

LaTeX

$$$AEMeasurable(f,\mu) \Rightarrow \bigl(\mathrm{IsProbabilityMeasure}(\mathrm{map}\ f\ mu) \iff \mathrm{IsProbabilityMeasure}(\mu)\bigr)$$$

Lean4

theorem isProbabilityMeasure_map_iff {μ : Measure α} {f : α → β} (hf : AEMeasurable f μ) :
    IsProbabilityMeasure (μ.map f) ↔ IsProbabilityMeasure μ :=
  ⟨fun _ ↦ isProbabilityMeasure_of_map hf, fun _ ↦ isProbabilityMeasure_map hf⟩

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