Theorems · Theorem · information theory

InformationTheory.toReal_klDiv_eq_integral_klFun

∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    (InformationTheory.klDiv μ ν).toReal = ∫ (x : α), InformationTheory.klFun (μ.rnDeriv ν x).toReal ∂ν

Defined in

Mathlib.InformationTheory.KullbackLeibler.Basic

Cited by

3 results in Mathlib

Foundations

Depth 268 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure