cdf_eq_real — Mathlib

English

For a probability measure μ, Fμ(x) equals μ.real(Iic x) for all x.

Русский

Для вероятностной меры μ Fμ(x) равно μ.real(Iic x) для всех x.

LaTeX

$$$ cdf(\mu)(x) = \mu.real(Iic x) $$$

Lean4

theorem cdf_eq_real (μ : Measure I) [IsProbabilityMeasure μ] (x : I) : cdf (μ.map Subtype.val) x.1 = μ.real (Icc 0 x) :=
  by
  haveI : IsProbabilityMeasure (μ.map Subtype.val) := isProbabilityMeasure_map (by fun_prop)
  rw [ProbabilityTheory.cdf_eq_real, map_measureReal_apply measurable_subtype_coe measurableSet_Iic, subtype_Iic_eq_Icc]

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