tendsto_rightDeriv_klFun_atTop

Mathlib.InformationTheory.KullbackLeibler.KLFun

URI: https://scilib.ai/kg/mathlib#InformationTheory.tendsto_rightDeriv_klFun_atTop

← MathLib Explorer

English

As x → +∞, the right derivative of klFun tends to +∞.

Русский

При x → +∞ правый предел производной klFun стремится к +∞.

LaTeX

$$$\\lim_{x \\to +\\infty} \\dfrac{d}{dx^+}\\mathrm{klFun}(x) = +\\infty$$$

Lean4

theorem tendsto_rightDeriv_klFun_atTop : Tendsto (fun x ↦ derivWithin klFun (Ioi x) x) atTop atTop :=
  by
  simp only [rightDeriv_klFun]
  exact tendsto_log_atTop

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

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

Разделы

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

Аффилиация

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