isProbabilityMeasure_comap — Mathlib

English

If f is injective and a.e.-membership and measurability conditions hold, then μ.comap f is a probability measure.

Русский

Если f инъективно и выполняются условия по членству и измеримости, то μ.comap f — вероятностная мера.

LaTeX

$$$\text{Injective}(f) \Rightarrow \mathrm{Event}(a\in\mathrm{range}(f)) \Rightarrow (\forall s, \text{MeasurableSet } s \Rightarrow \text{MeasurableSet}(f''s)) \Rightarrow \mathrm{IsProbabilityMeasure}(\mu\comap f)$$$

Lean4

theorem isProbabilityMeasure_comap (hf : Injective f) (hf' : ∀ᵐ a ∂μ, a ∈ range f)
    (hf'' : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) : IsProbabilityMeasure (μ.comap f) where
  measure_univ :=
    by
    rw [comap_apply _ hf hf'' _ MeasurableSet.univ, ← mem_ae_iff_prob_eq_one (hf'' _ MeasurableSet.univ)]
    simpa

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