measure_condCDF_Iic

Mathlib.Probability.Kernel.Disintegration.CondCDF

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

← MathLib Explorer

English

For every a, condCDF ρ a tends to 1 as x → +∞.

Русский

Для каждого a condCDF ρ a стремится к 1 при x → +∞.

LaTeX

$$$\\lim_{x \\to +\\infty} condCDF(ρ,a)(x) = 1.$$$

Lean4

theorem measure_condCDF_Iic (ρ : Measure (α × ℝ)) (a : α) (x : ℝ) :
    (condCDF ρ a).measure (Iic x) = ENNReal.ofReal (condCDF ρ a x) :=
  by
  rw [← sub_zero (condCDF ρ a x)]
  exact (condCDF ρ a).measure_Iic (tendsto_condCDF_atBot ρ a) _

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

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

Разделы

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

Аффилиация

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