Pinsker's inequality

For probability measures μ and ν and a measurable event s, 2 (μ s - ν s)² ≤ klDiv μ ν, the Kullback–Leibler divergence in nats (Cslib.Probability.ofReal_two_mul_sq_measureReal_sub_le_klDiv). The proof is the variational one: Gibbs' inequality for an exponentially tilted measure (Mathlib's integral_llr_tilted_right) and Hoeffding's lemma for the indicator of the event. A Hahn decomposition then gives the form with Mathlib's total variation distance, tvDist μ ν ^ 2 / 2 ≤ klDiv μ ν (Cslib.Probability.ofReal_tvDist_sq_div_two_le_klDiv). The finite-distribution forms, in terms of statistical distance, are in Probability/Divergence.

Main results

• Cslib.Probability.ofReal_two_mul_sq_measureReal_sub_le_klDiv: Pinsker for an event.
• Cslib.Probability.ofReal_tvDist_sq_div_two_le_klDiv: Pinsker with Mathlib's tvDist.

References

• T. M. Cover, J. A. Thomas, Elements of Information Theory, Lemma 11.6.1.

theorem Cslib.Probability.ofReal_two_mul_sq_measureReal_sub_le_klDiv {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {s : Set α} (hs : MeasurableSet s) : ENNReal.ofReal (2 * (μ.real s - ν.real s) ^ 2) ≤ InformationTheory.klDiv μ ν

Pinsker's inequality for a single event: 2 (μ s - ν s)² ≤ klDiv μ ν, the divergence in nats, for probability measures and a measurable event s. The statement holds unconditionally since klDiv μ ν = ∞ when μ is not absolutely continuous with respect to ν or the log-likelihood ratio is not integrable.

theorem Cslib.Probability.ofReal_tvDist_sq_div_two_le_klDiv {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : ENNReal.ofReal (MeasureTheory.tvDist μ ν ^ 2 / 2) ≤ InformationTheory.klDiv μ ν

Pinsker's inequality with Mathlib's total variation distance tvDist, which takes values in [0, 2] for probability measures: tvDist μ ν ^ 2 / 2 ≤ klDiv μ ν, the divergence in nats. It follows from the event form applied to a Hahn decomposition.