InformationTheory.Shannon.DPI
Data processing inequality for mutual information #
The data processing inequality I(X; f(Y)) ≤ I(X; Y) for deterministic post-processing.
Main statements #
klDiv_map_le—klDiv (μ.map f) (ν.map f) ≤ klDiv μ νfor any measurablef.mutualInfo_le_of_postprocess—I(X; f(Y)) ≤ I(X; Y).
Implementation notes #
klDiv_map_le is built via conditional Jensen (ConvexOn.map_condExp_le) applied to
klFun and the Radon-Nikodym derivative identity Measure.rnDeriv_map.
The mutual-information bound follows by applying klDiv_map_le to Prod.map id f.
InformationTheory.Shannon.klDiv_map_le
source{α : Type u_5}
{β : Type u_6}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
(hf : Measurable f)
(μ ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
General pushforward DPI: klDiv (μ.map f) (ν.map f) ≤ klDiv μ ν for measurable f.
Used by
InformationTheory.Shannon.mutualInfo_le_of_postprocess
source{Ω : Type u_1}
[MeasurableSpace Ω]
{X : Type u_2}
[MeasurableSpace X]
{Y : Type u_3}
[MeasurableSpace Y]
{Z : Type u_4}
[MeasurableSpace Z]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(Xs : Ω → X)
(Yo : Ω → Y)
(hXs : Measurable Xs)
(hYo : Measurable Yo)
{f : Y → Z}
(hf : Measurable f)
:
Data processing inequality: I(X; f(Y)) ≤ I(X; Y) for measurable f.