Theorems · Theorem · information theory

InformationTheory.integral_llr_add_mul_log_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.log (ν.real Set.univ) + 1 - μ.real Set.univ

Defined in

Mathlib.InformationTheory.KullbackLeibler.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure