defaultRatCDF_nonneg

Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

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

English

defaultRatCDF equals piecewise 0 or 1 depending on q<0.

Русский

defaultRatCDF равен 0 при q<0 и 1 при q≥0.

LaTeX

$$$\\mathrm{defaultRatCDF}(q) = \\begin{cases}0 & q<0 \\\\ 1 & q\\ge 0\\end{cases}$$$

Lean4

theorem defaultRatCDF_nonneg (q : ℚ) : 0 ≤ defaultRatCDF q :=
  by
  unfold defaultRatCDF
  split_ifs
  exacts [le_rfl, zero_le_one]

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

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

Разделы

Аффилиация

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