isProbabilityMeasure_map — Mathlib

English

If f is almost everywhere measurable with respect to μ, then the pushforward measure map f μ is a probability measure.

Русский

Если f почти наверняка измеримо относительно μ, то образующая мера map f μ — вероятностная.

LaTeX

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

Lean4

theorem isProbabilityMeasure_map {f : α → β} (hf : AEMeasurable f μ) : IsProbabilityMeasure (map f μ) :=
  ⟨by simp [map_apply_of_aemeasurable, hf]⟩

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