The divergence from the uniform law is at most its chi-squared distance

Category: 1-Mathlib (CSD-free). BACKLOG #130's first half.

Mathlib has the Kullback-Leibler divergence and no comparison inequality for it. The one a rate argument reaches for is the chi-squared bound: klDiv is at most the chi-squared distance, which is quadratic in the deviation and therefore converts an L² estimate into a divergence estimate. Against the uniform law on a finite type with n points the chi-squared distance is n · ∑ (p x − 1/n)², and that is the form proved here.

• ★★★ log_card_sub_measureEntropy_le_chiSq — the real-valued inequality log n − H(μ) ≤ n · ∑ (μ{x} − 1/n)²;
• ★★★ klDiv_uniformOn_univ_le_chiSq — the same read through klDiv_uniformOn_univ, which is the statement a consumer uses.

How it goes

Both sides are the same sum, compared pointwise. Writing p x for μ.real {x}:

• the left side is ∑ p x · log (n · p x), because ∑ p x = 1 turns log n into ∑ p x · log n and the p x = 0 terms contribute nothing to either half;
• log t ≤ t − 1 (Real.log_le_sub_one_of_pos) at t = n · p x, multiplied by p x ≥ 0, gives p x · log (n · p x) ≤ p x · (n · p x − 1) — the only analysis in the file;
• and ∑ p x · (n · p x − 1) = n · ∑ p x² − 1 is equal to n · ∑ (p x − 1/n)², again by ∑ p x = 1. So the inequality is tight exactly where log t = t − 1, at p x = 1/n.

Honest scope

⚠️ Uniform reference only. The general bound klDiv μ ν ≤ ∑ (μ{x} − ν{x})²/ν{x} needs the Radon-Nikodym derivative of μ against an arbitrary ν, which FiniteEntropy.lean computes only for the uniform law (withDensity_uniformOn_univ). A consumer whose reference is uniform as a theorem can use this; one whose reference is merely believed uniform has to carry that as a hypothesis.

⚠️ Finite type only, and both measures are probability measures: klDiv's correction terms are dropped by klDiv_uniformOn_univ, which assumes it.

⚠️ It is an inequality, not an equivalence. The chi-squared distance can be arbitrarily larger than the divergence, so a chi-squared bound that fails to tend to zero says nothing about klDiv.

References

T. Cover, J. Thomas, Elements of Information Theory, 2nd ed., §11.6 (the chi-squared comparison); FiniteEntropy.lean (measureEntropy, klDiv_uniformOn_univ, sum_measureReal_singleton); Mathlib.Analysis.SpecialFunctions.Log.Basic (Real.log_le_sub_one_of_pos); specs/future-work.md; specs/BACKLOG.md #130, #118.

theorem InformationTheory.log_card_sub_measureEntropy_le_chiSq {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] [Nonempty α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : Real.log ↑(Fintype.card α) - measureEntropy μ ≤ ↑(Fintype.card α) * ∑ x : α, (μ.real {x} - (↑(Fintype.card α))⁻¹) ^ 2

★★★ The entropy defect is at most the chi-squared distance from the uniform law.

log n − H(μ) ≤ n · ∑ (μ{x} − 1/n)², where n is the cardinality. Both sides are the same sum read two ways, compared pointwise by log t ≤ t − 1.

theorem InformationTheory.klDiv_uniformOn_univ_le_chiSq {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] [Nonempty α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : klDiv μ (ProbabilityTheory.uniformOn Set.univ) ≤ ENNReal.ofReal (↑(Fintype.card α) * ∑ x : α, (μ.real {x} - (↑(Fintype.card α))⁻¹) ^ 2)

★★★ The chi-squared bound on the divergence from the uniform law. This is the form a rate argument consumes: an L² estimate on the point masses bounds klDiv, at the cost of one factor of the cardinality.