measure_cdf — Mathlib

English

For a Stieltjes function f, the cdf of its associated measure equals f when f is normalized by limits 0 and 1: cdf f.measure = f.

Русский

Для функции Стилтьджеса f мера f.measure имеет cdf, равную самой f при нормировке пределами 0 и 1: cdf f.measure = f.

LaTeX

$$$ cdf(f.measure) = f $$$

Lean4

/-- The measure associated to the cdf of a probability measure is the same probability measure. -/
theorem measure_cdf [IsProbabilityMeasure μ] : (cdf μ).measure = μ :=
  by
  refine ext_of_Iic (cdf μ).measure μ (fun a ↦ ?_)
  rw [StieltjesFunction.measure_Iic _ (tendsto_cdf_atBot μ), sub_zero, ofReal_cdf]

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