Pinsker's inequality (total variation and Kullback–Leibler divergence) #

For probability measures P, Q on a finite alphabet α with P ≪ Q, the total-variation norm tvNorm P Q := (1/2) * ∑ x, |P.real {x} - Q.real {x}| is bounded by the square root of the Kullback–Leibler divergence: tvNorm P Q ≤ √((klDiv P Q).toReal).

This is the weak form with constant 1; the sharp Cover–Thomas form tvNorm P Q ≤ √((klDiv P Q).toReal / 2) is proved separately in Pinsker/Sharp.lean.

Main definitions #

• tvNorm — the total-variation norm between two probability measures on a finite alphabet.

Main statements #

• klFun_ge_sub_sqrt_sq — the pointwise Bretagnolle–Huber bound (√t - 1)^2 ≤ klFun t.
• tvNorm_le_sqrt_klDiv — Pinsker's inequality (weak form) tvNorm P Q ≤ √((klDiv P Q).toReal).

Implementation notes #

The proof combines the pointwise Bretagnolle–Huber bound klFun t ≥ (√t - 1)^2 with the Cauchy–Schwarz factorization |p - q| = |√p - √q| · (√p + √q), bounding ∑ (√p + √q)^2 ≤ 4.

References #

• T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

Bretagnolle–Huber pointwise inequality #

Cauchy-Schwarz and sum bound helpers #

Total variation and Pinsker's inequality #