klDiv_zero_left

Mathlib.InformationTheory.KullbackLeibler.Basic

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

← MathLib Explorer

English

If ν is finite, then KL(0, ν) = ν(univ).

Русский

Если ν конечна, то KL(0, ν) = ν(univ).

LaTeX

$$$klDiv\\,0\\,ν = ν(univ)$$$

Lean4

@[simp]
theorem klDiv_zero_left [IsFiniteMeasure ν] : klDiv 0 ν = ν univ :=
  by
  convert klDiv_of_ac_of_integrable (Measure.AbsolutelyContinuous.zero _) integrable_zero_measure
  simp

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

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

Разделы

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

Аффилиация

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