Pinsker's inequality

Pinsker's inequality bounds total variation by relative entropy, with natural logarithms. We use Mathlib's InformationTheory.klDiv and total variation distance etvDist. The latter is the signed-measure norm, twice the usual total-variation distance for probability measures. Thus etvDist_sq_le_two_mul_klDiv states the classical bound dTV(μ, ν)² ≤ klDiv μ ν / 2. For finite measures with common mass M, etvDist_sq_le_two_mul_mass_mul_klDiv gives the rescaled bound ‖μ - ν‖² ≤ 2 * M * klDiv μ ν. Both include infinite entropy and require only a measurable space; the finite-measure version also covers zero mass.

The measurable-event versions are two_mul_sq_measureReal_sub_le_klDiv and two_mul_sq_measureReal_sub_le_mul_klDiv. They use real subtraction before squaring, so they control the absolute difference in both directions.

These bounds turn small relative entropy into uniform control of probabilities of measurable events and of the total-variation distance.

theorem TauCeti.two_mul_sq_measureReal_sub_le_klDiv {α : Type u_1} [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 events, with natural logarithms. The extended-valued right side includes infinite relative entropy, without an absolute-continuity hypothesis.

theorem TauCeti.two_mul_sq_measureReal_sub_le_mul_klDiv {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hmass : μ Set.univ = ν Set.univ) {s : Set α} (hs : MeasurableSet s) : ENNReal.ofReal (2 * (μ.real s - ν.real s) ^ 2) ≤ μ Set.univ * InformationTheory.klDiv μ ν

The event form of Pinsker's inequality for finite measures of equal mass M: 2 * (μ s - ν s)² ≤ M * klDiv μ ν. This also covers zero mass and infinite entropy.

theorem TauCeti.etvDist_sq_le_two_mul_mass_mul_klDiv {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hmass : μ Set.univ = ν Set.univ) : MeasureTheory.etvDist μ ν ^ 2 ≤ 2 * μ Set.univ * InformationTheory.klDiv μ ν

Pinsker's inequality for finite measures of equal mass, using Mathlib's total variation distance etvDist, the signed-measure norm. If their common mass is M, this says ‖μ - ν‖² ≤ 2 * M * klDiv μ ν. There is no finiteness assumption on relative entropy.

theorem TauCeti.etvDist_sq_le_two_mul_klDiv {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.etvDist μ ν ^ 2 ≤ 2 * InformationTheory.klDiv μ ν

Pinsker's inequality for probability measures, with natural logarithms and no absolute-continuity assumption. Mathlib's etvDist on the left is twice the usual distance dTV(μ, ν) = sup_s |μ s - ν s|, so the bound is equivalently 2 * dTV(μ, ν)² ≤ klDiv μ ν.