Pinsker's Inequality

This file states Pinsker's inequality relating total variation distance and KL divergence.

theorem CommunicationComplexity.pinsker_inequality {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) : ENNReal.ofReal (2 * tvDistance μ ν ^ 2) ≤ InformationTheory.klDiv ↑μ ↑ν

Pinsker's inequality: total variation distance is bounded by KL divergence. This is stated in the ℝ≥0∞ form 2 * TV^2 ≤ KL, using natural logarithms in Mathlib's KL divergence.

theorem CommunicationComplexity.two_mul_tvDistance_sq_le_toReal_klDiv {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) (hkl : InformationTheory.klDiv ↑μ ↑ν ≠ ⊤) : 2 * tvDistance μ ν ^ 2 ≤ (InformationTheory.klDiv ↑μ ↑ν).toReal

Real-valued Pinsker corollary, useful once the relevant KL divergence is known to be finite.