Theorems · Theorem · information theory

InformationTheory.integral_llr_add_sub_measure_univ_nonneg

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

Gibbs' inequality: the Kullback-Leibler divergence is nonnegative. Note that since klDiv takes value in ℝ≥0∞ (defined when it is finite as ENNReal.ofReal (...)), it is nonnegative by definition. This lemma proves that the argument of ENNReal.ofReal is also nonnegative.

Defined in

Mathlib.InformationTheory.KullbackLeibler.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure