Theorems · Theorem · information theory

InformationTheory.toReal_klDiv_trim_of_ac

∀ {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] (hm : m ≤ m𝓧),
  μ.AbsolutelyContinuous ν →
    (InformationTheory.klDiv (μ.trim hm) (ν.trim hm)).toReal =
      ∫ (x : 𝓧), InformationTheory.klFun (ν[fun x => (μ.rnDeriv ν x).toReal | m] x) ∂ν

Defined in

Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure