isProbabilityMeasure_of_map — Mathlib

English

If f is almost everywhere measurable, then μ.map f is a probability measure iff μ is a probability measure.

Русский

Если f почти наверняка измеримо, тогда μ.map f является вероятностной мерой тогда и только тогда, когда μ — вероятностная мера.

LaTeX

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

Lean4

theorem isProbabilityMeasure_of_map {μ : Measure α} {f : α → β} (hf : AEMeasurable f μ)
    [IsProbabilityMeasure (μ.map f)] : IsProbabilityMeasure μ where
  measure_univ := by
    rw [← Set.preimage_univ (f := f), ← map_apply_of_aemeasurable hf .univ]
    exact IsProbabilityMeasure.measure_univ

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