Theorems · Theorem · information theory

InformationTheory.klDiv_compProd_eq_add

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

Chain rule for the Kullback-Leibler divergence, with conditional KL expressed using composition-products. This version holds without any assumption on the measurable spaces.

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites34

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

DFunLike.coeproof · cited by 62,936
Realproof · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement and proof · cited by 9,879
Top.topproof · cited by 9,680
Set.univproof · cited by 3,945
mul_oneproof · cited by 3,885
add_zeroproof · cited by 2,707
MeasureTheory.integralproof · cited by 1,779
MeasureTheory.Integrableproof · cited by 1,367
ProbabilityTheory.Kernelstatement and proof · cited by 1,281

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.