cdf_measure_stieltjesFunction — Mathlib

English

Let μ be a probability measure on the unit interval. Then for x in I, the cdf of μ mapped to the real line satisfies a specific relation with μ.real on Icc 0 x.

Русский

Пусть μ — вероятность на единичном интервале. Тогда для x ∈ I выполняется равенство, связывающее cdf(μ.map Subtype.val) и μ.real(Icc 0 x).

LaTeX

$$$ \forall x \in I,\ cdf( (μ.map Subtype\!\!{val}) ).toFun x.1 = μ.real(Icc 0 x) $$$

Lean4

theorem cdf_measure_stieltjesFunction (f : StieltjesFunction) (hf0 : Tendsto f atBot (𝓝 0))
    (hf1 : Tendsto f atTop (𝓝 1)) : cdf f.measure = f :=
  by
  refine (cdf f.measure).eq_of_measure_of_tendsto_atBot f ?_ (tendsto_cdf_atBot _) hf0
  have h_prob : IsProbabilityMeasure f.measure := ⟨by rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]⟩
  exact measure_cdf f.measure

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