Theorems · Theorem · information theory

InformationTheory.integrable_klFun_rnDeriv_iff

∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    (MeasureTheory.Integrable (fun x => InformationTheory.klFun (μ.rnDeriv ν x).toReal) ν ↔
      MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ)

For two finite measures μ ≪ ν, the function x ↦ klFun (μ.rnDeriv ν x).toReal is integrable with respect to ν iff llr μ ν is integrable with respect to μ.

Defined in

Mathlib.InformationTheory.KullbackLeibler.KLFun

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure