le_one

Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.IsMeasurableRatCDF.le_one

← MathLib Explorer

English

defaultRatCDF equals the piecewise 0 or 1 according to 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 le_one {f : α → ℚ → ℝ} (hf : IsMeasurableRatCDF f) (a : α) (q : ℚ) : f a q ≤ 1 :=
  Monotone.ge_of_tendsto (hf.isRatStieltjesPoint a).mono (hf.isRatStieltjesPoint a).tendsto_atTop_one q

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

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

Разделы

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

Аффилиация

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