tendsto_defaultRatCDF_atBot

Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

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

← MathLib Explorer

English

The limit of defaultRatCDF along atBot equals 0.

Русский

Предел along atBot равен 0.

LaTeX

$$$\\mathrm{Tendsto}(\\mathrm{defaultRatCDF},\\mathrm{atBot},(\\mathcal{N}))$ to 0$$

Lean4

theorem tendsto_defaultRatCDF_atBot : Tendsto defaultRatCDF atBot (𝓝 0) :=
  by
  refine (tendsto_congr' ?_).mp tendsto_const_nhds
  rw [EventuallyEq, eventually_atBot]
  refine ⟨-1, fun q hq => (if_pos (hq.trans_lt ?_)).symm⟩
  linarith

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

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

Разделы

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

Аффилиация

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