isProbabilityMeasure — Mathlib

English

The measure p.toMeasure is a probability measure on α; its total mass is 1.

Русский

Мера p.toMeasure является вероятностной мерой на α; её масса total равна 1.

LaTeX

$$$\\text{IsProbabilityMeasure}(p.toMeasure)$$$

Lean4

/-- The measure associated to a `PMF` by `toMeasure` is a probability measure. -/
instance isProbabilityMeasure [MeasurableSpace α] (p : PMF α) : IsProbabilityMeasure p.toMeasure :=
  ⟨by
    simpa only [MeasurableSet.univ, toMeasure_apply_eq_toOuterMeasure_apply, Set.indicator_univ, toOuterMeasure_apply,
      ENNReal.coe_eq_one] using tsum_coe p⟩

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