cdf_nonneg

Mathlib.Probability.CDF

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

English

The cumulative distribution function is nonnegative for all x.

Русский

Функция распределения неотрицательна для всех x.

LaTeX

$$$$0 \le \mathrm{cdf}(\mu)(x)\quad\text{for all } x\in\mathbb{R}.$$$

Lean4

/-- The cdf is non-negative. -/
theorem cdf_nonneg (x : ℝ) : 0 ≤ cdf μ x :=
  condCDF_nonneg _ _ _

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

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

Разделы

Аффилиация

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