Theorems · Theorem · information theory

InformationTheory.integral_klFun_rnDeriv

∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
      ∫ (x : α), InformationTheory.klFun (μ.rnDeriv ν x).toReal ∂ν =
        ∫ (x : α), MeasureTheory.llr μ ν x ∂μ + ν.real Set.univ - μ.real Set.univ

Defined in

Mathlib.InformationTheory.KullbackLeibler.KLFun

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure