strictConvexOn_klFun

Mathlib.InformationTheory.KullbackLeibler.KLFun

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

← MathLib Explorer

English

The function klFun is strictly convex on the interval [0, ∞).

Русский

Функция klFun строго выпукла на интервале [0, ∞).

LaTeX

$$StrictConvexOn ℝ (Ici 0) klFun$$

Lean4

/-- `klFun` is strictly convex on [0,∞). -/
theorem strictConvexOn_klFun : StrictConvexOn ℝ (Ici 0) klFun :=
  (strictConvexOn_mul_log.add_convexOn (convexOn_const _ (convex_Ici _))).sub_concaveOn (concaveOn_id (convex_Ici _))

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

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

Разделы

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

Аффилиация

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