Data processing inequality for the Kullback-Leibler divergence

The data processing inequality is a way to express the intuition that applying a (possibly random) transformation to random variables cannot increase the information they contain.

Main statements

We prove three versions of the data processing inequality for the Kullback-Leibler divergence, for measurable maps, restrictions to sub-sigma-algebras, and composition with Markov kernels. Let μ, ν be finite measures on 𝓧, with sigma-algebra m𝓧.

• klDiv_map_le: klDiv (μ.map g) (ν.map g) ≤ klDiv μ ν for a measurable function g.
• klDiv_trim_le: klDiv (μ.trim hm) (ν.trim hm) ≤ klDiv μ ν for a sub-sigma-algebra m of m𝓧 (with hm : m ≤ m𝓧).
• klDiv_comp_right_le: klDiv (κ ∘ₘ μ) (κ ∘ₘ ν) ≤ klDiv μ ν for a Markov kernel κ.

theorem ConvexOn.map_condExp_rnDeriv_le {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} (hm : m ≤ m𝓧) (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Set.Ici 0) 0) (h_int : MeasureTheory.Integrable (fun (x : 𝓧) => f (μ.rnDeriv ν x).toReal) ν) : (fun (x : 𝓧) => f (ν[fun (x : 𝓧) => (μ.rnDeriv ν x).toReal | m] x)) ≤ᵐ[ν.trim hm] ν[fun (x : 𝓧) => f (μ.rnDeriv ν x).toReal | m]

theorem ConvexOn.comp_rnDeriv_map_le {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} {g : 𝓧 → 𝓨} (hμν : μ.AbsolutelyContinuous ν) (hg : Measurable g) (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Set.Ici 0) 0) (h_int : MeasureTheory.Integrable (fun (x : 𝓧) => f (μ.rnDeriv ν x).toReal) ν) : (fun (x : 𝓧) => f ((MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) (g x)).toReal) ≤ᵐ[ν] ν[fun (x : 𝓧) => f (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨]

theorem ConvexOn.integrable_comp_rnDeriv_map {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} {g : 𝓧 → 𝓨} (hμν : μ.AbsolutelyContinuous ν) (hg : Measurable g) (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Set.Ici 0) 0) (h_int : MeasureTheory.Integrable (fun (x : 𝓧) => f (μ.rnDeriv ν x).toReal) ν) : MeasureTheory.Integrable (fun (x : 𝓨) => f ((MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) x).toReal) (MeasureTheory.Measure.map g ν)

theorem ConvexOn.comp_rnDeriv_trim_le {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} (hm : m ≤ m𝓧) (hμν : μ.AbsolutelyContinuous ν) (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Set.Ici 0) 0) (h_int : MeasureTheory.Integrable (fun (x : 𝓧) => f (μ.rnDeriv ν x).toReal) ν) : (fun (x : 𝓧) => f ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) ≤ᵐ[ν.trim hm] ν[fun (x : 𝓧) => f (μ.rnDeriv ν x).toReal | m]

theorem ConvexOn.integrable_comp_rnDeriv_trim {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} (hm : m ≤ m𝓧) (hμν : μ.AbsolutelyContinuous ν) (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Set.Ici 0) 0) (h_int : MeasureTheory.Integrable (fun (x : 𝓧) => f (μ.rnDeriv ν x).toReal) ν) : MeasureTheory.Integrable (fun (x : 𝓧) => f ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) (ν.trim hm)

theorem ConvexOn.integrable_comp_condExp_rnDeriv {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} (hm : m ≤ m𝓧) (hμν : μ.AbsolutelyContinuous ν) (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Set.Ici 0) 0) (h_int : MeasureTheory.Integrable (fun (x : 𝓧) => f (μ.rnDeriv ν x).toReal) ν) : MeasureTheory.Integrable (fun (x : 𝓧) => f (ν[fun (x : 𝓧) => (μ.rnDeriv ν x).toReal | m] x)) ν

theorem InformationTheory.integrable_llr_map {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {g : 𝓧 → 𝓨} (hμν : μ.AbsolutelyContinuous ν) (hg : Measurable g) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : MeasureTheory.Integrable (MeasureTheory.llr (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν)) (MeasureTheory.Measure.map g μ)

theorem InformationTheory.toReal_klDiv_map_of_ac {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {g : 𝓧 → 𝓨} (hμν : μ.AbsolutelyContinuous ν) (hg : Measurable g) : (klDiv (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν)).toReal = ∫ (x : 𝓧), klFun (ν[fun (x : 𝓧) => (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν

theorem InformationTheory.klDiv_map_of_ac {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {g : 𝓧 → 𝓨} (hμν : μ.AbsolutelyContinuous ν) (hg : Measurable g) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : klDiv (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν) = ENNReal.ofReal (∫ (x : 𝓧), klFun (ν[fun (x : 𝓧) => (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν)

theorem InformationTheory.toReal_klDiv_trim_of_ac {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hm : m ≤ m𝓧) (hμν : μ.AbsolutelyContinuous ν) : (klDiv (μ.trim hm) (ν.trim hm)).toReal = ∫ (x : 𝓧), klFun (ν[fun (x : 𝓧) => (μ.rnDeriv ν x).toReal | m] x) ∂ν

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

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

theorem InformationTheory.klDiv_trim_le {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} (μ ν : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hm : m ≤ m𝓧) : klDiv (μ.trim hm) (ν.trim hm) ≤ klDiv μ ν

Data processing inequality for the Kullback-Leibler divergence and sub-sigma-algebras.

theorem 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 κ] : klDiv (μ.bind ⇑κ) (ν.bind ⇑κ) ≤ klDiv μ ν

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