Theorems · Theorem · information theory

InformationTheory.klDiv_comp_right_le

∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} (μ ν : MeasureTheory.Measure 𝓧)
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel 𝓧 𝓨)
  [ProbabilityTheory.IsMarkovKernel κ], InformationTheory.klDiv (μ.bind ⇑κ) (ν.bind ⇑κ) ≤ InformationTheory.klDiv μ ν

The Data Processing Inequality for the Kullback-Leibler divergence and a Markov kernel.

Defined in: Mathlib.InformationTheory.KullbackLeibler.DataProcessing
Cited by: 0 results in Mathlib
Foundations: Depth 313 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasureTheory.IsFiniteMeasure MeasureTheory.IsFiniteMeasure ProbabilityTheory.IsMarkovKernel

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement · cited by 9,879
ProbabilityTheory.Kernelstatement and proof · cited by 1,281
MeasureTheory.IsFiniteMeasurestatement and proof · cited by 1,078
MeasureTheory.Measure.bindstatement and proof · cited by 173
MeasureTheory.Measure.compProdproof · cited by 132
ProbabilityTheory.IsMarkovKernelstatement and proof · cited by 124
measurable_sndproof · cited by 94
InformationTheory.klDivstatement and proof · cited by 34
MeasureTheory.Measure.sndproof · cited by 21

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.