Theorems · Theorem · information theory

InformationTheory.klDiv_map_le

∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} (μ ν : MeasureTheory.Measure 𝓧)
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {g : 𝓧 → 𝓨},
  Measurable g →
    InformationTheory.klDiv (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν) ≤
      InformationTheory.klDiv μ ν

Data processing inequality for the Kullback-Leibler divergence and measurable functions.

Defined in

Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure