Data-processing inequality for Kullback–Leibler divergence

Proved

InformationTheory.klDiv_map_le

by Harry_Xu · Aug 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

data-processinginformation-theorykullback-leibler

Let $P$ and $Q$ be finite measures on a standard Borel measurable space $\Omega$ , and let $\varphi:\Omega\to\mathcal Y$ be a measurable observation map into an arbitrary measurable space. If $P_\varphi$ and $Q_\varphi$ denote the pushforward laws, then

D(P_\varphi\Vert Q_\varphi)\le D(P\Vert Q).

Thus applying any measurable data transformation cannot increase relative entropy. The arbitrary target measurable space is important for finite-feedback partial monitoring, where the supplied signal sigma-algebra need not be discrete.

Preamble

import Mathlib.InformationTheory.KullbackLeibler.Basic

open MeasureTheory ProbabilityTheory InformationTheory
open scoped ENNReal

Formal statement

theorem InformationTheory.klDiv_map_le
    {α β : Type*} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
    [MeasurableSpace β] (φ : α → β) (hφ : Measurable φ)
    (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    klDiv (μ.map φ) (ν.map φ) ≤ klDiv μ ν := by
  sorry

Source

Lattimore and Szepesvari, Bandit Algorithms (Cambridge University Press, 2020), Chapter 14, Exercise 14.10 (data processing inequality), p. 196, together with Exercise 14.9 (pushforward measures), pp. 195–196; applied explicitly in Theorem 37.12 Step 2, p. 490.

View graph