klDiv_ne_top_iff

Mathlib.InformationTheory.KullbackLeibler.Basic

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

English

KL(μ, ν) ≠ ∞ iff μ ≪ ν and Integrable(llr μ ν) μ.

Русский

KL(μ, ν) ≠ ∞ тогда и только тогда, когда μ ≪ ν и llr интегрируем по μ.

LaTeX

$$$klDiv\\,\\mu\\,\\nu \\neq \\infty \\,\\iff \\,\\mu\\ll\\nu \\\\land \\\\ Integrable(llr\\,\\mu\\,\\nu)\\,\\mu$$$

Lean4

theorem klDiv_ne_top_iff : klDiv μ ν ≠ ∞ ↔ μ ≪ ν ∧ Integrable (llr μ ν) μ := by simp [ne_eq, klDiv_eq_top_iff]

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

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

Разделы

Аффилиация

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