Sharp Pinsker inequality (constant 1/√2) #

For probability measures P, Q on a finite alphabet α with P ≪ Q, the sharp Cover–Thomas form of Pinsker's inequality: tvNorm P Q ≤ √((klDiv P Q).toReal / 2). The total-variation norm tvNorm is shared with the weak form in Pinsker/Basic.lean.

Main statements #

• klFun_sharp_lower — the pointwise sharp bound 3 * (t - 1)^2 ≤ 2 * (t + 2) * klFun t.
• tvNorm_le_sqrt_klDiv_div_two — the sharp Pinsker inequality tvNorm P Q ≤ √((klDiv P Q).toReal / 2).

Implementation notes #

The pointwise bound is obtained from the auxiliary H t := 2 (t + 2) · klFun t - 3 (t - 1)^2, whose second derivative 4 (log t + 1/t - 1) is nonnegative on (0, ∞) and which has a minimum of 0 at t = 1. The global bound follows by a per-element application together with the Cauchy–Schwarz step and ∑ (p + 2q) = 3.

References #

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

Pointwise sharp Pinsker inequality #

Sharp Pinsker inequality #