instIsProbabilityMeasurecdf — Mathlib

English

If μ is a probability measure, then the measure associated to its cdf is again a probability measure: (cdf μ).measure is a probability measure.

Русский

Если μ — вероятностная мера, то мера, связанная с её ФП, снова является вероятностной мерой: (cdf μ).measure.

LaTeX

$$$ IsProbabilityMeasure( (cdf(\mu)).measure ) $$$

Lean4

instance instIsProbabilityMeasurecdf : IsProbabilityMeasure (cdf μ).measure :=
  by
  constructor
  simp only [StieltjesFunction.measure_univ _ (tendsto_cdf_atBot μ) (tendsto_cdf_atTop μ), sub_zero, ENNReal.ofReal_one]

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