ofReal_cdf — Mathlib

English

For a probability measure μ on ℝ, the extended-real value of the cdf equals the real measure of the left-closed interval: ENNReal.ofReal (cdf μ x) = μ (Iic x).

Русский

Для μ — вероятность на ℝ имеет место равенство ENNReal.ofReal(Fμ(x)) = μ((-∞, x]).

LaTeX

$$$ \forall x \in \mathbb{R},\ ENNReal.ofReal (cdf(\mu)(x)) = \mu(Iic\,x) $$$

Lean4

theorem ofReal_cdf [IsProbabilityMeasure μ] (x : ℝ) : ENNReal.ofReal (cdf μ x) = μ (Iic x) :=
  by
  have h := lintegral_condCDF ((dirac Unit.unit).prod μ) x
  simpa only [fst_prod, prod_prod, measure_univ, one_mul, lintegral_dirac] using h

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