monotone_cdf

Mathlib.Probability.CDF

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

English

Let μ be a measure on ℝ. The cdf is monotone: if x ≤ y then cdf μ x ≤ cdf μ y.

Русский

Пусть μ — мера на ℝ. Функция распределения неубывающая: если x ≤ y, то Fμ(x) ≤ Fμ(y).

LaTeX

$$$ \forall x,y \in \mathbb{R},\ x \le y \implies cdf(\mu)(x) \le cdf(\mu)(y) $$$

Lean4

/-- The cdf is monotone. -/
theorem monotone_cdf : Monotone (cdf μ) :=
  (condCDF _ _).mono

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

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

Разделы

Аффилиация

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