cdf_eq_real

Mathlib.Probability.CDF

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.cdf_eq_real

← MathLib Explorer

English

If μ is a probability measure, then Fμ(x) = μ.real((-∞, x]).

Русский

Если μ — вероятность, то Fμ(x) = μ.real((-∞, x]).

LaTeX

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

Lean4

theorem cdf_eq_real [IsProbabilityMeasure μ] (x : ℝ) : cdf μ x = μ.real (Iic x) := by
  rw [measureReal_def, ← ofReal_cdf μ x, ENNReal.toReal_ofReal (cdf_nonneg μ x)]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru