Convexity of relative entropy in its first measure

For a fixed finite reference measure ρ, relative entropy is convex in the measure being compared to ρ. On its finite-value domain it is strictly convex: mixing two distinct finite measures with positive weights gives strictly less than their weighted entropies. This is the uniqueness mechanism for entropy minimization over convex sets of measures, in particular sets with prescribed marginals.

The statements use Mathlib's finite-measure I-divergence InformationTheory.klDiv, including its mass correction. Neither normalization nor a topology on the measurable carrier is needed. Infinite values are retained in the convexity inequality; strictness requires both endpoint values to be finite. Equality for an interior mixture holds exactly when the measures agree.

For absolutely continuous measures, relative entropy is the integral of InformationTheory.klFun of the Radon–Nikodym density. Strict convexity of this integrand on [0, ∞) forces those densities to agree almost everywhere in the equality case.

Strict convexity also holds quantitatively. The midpoint convexity defect of klFun at two nonnegative reals bounds the square of their distance relative to their sum, and integrating this bound shows that the convexity defect of relative entropy at the midpoint of two measures controls the L¹(ρ) distance of their densities, that is, their total variation distance. This is the estimate that makes a minimizing sequence of an entropy minimization problem over a convex set of measures a Cauchy sequence.

References

• Mathlib, InformationTheory.klDiv_eq_lintegral_klFun_of_ac and InformationTheory.strictConvexOn_klFun.
• I. Csiszár, I-divergence geometry of probability distributions and minimization problems, Ann. Probability 3 (1975), 146–158. The quantitative midpoint estimate plays the role of the parallelogram identity in the proof of his Theorem 2.1.

theorem TauCeti.klDiv_smul_add_smul_le {α : Type u_1} [MeasurableSpace α] {μ ν ρ : MeasureTheory.Measure α} {a b : NNReal} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ρ] (hab : a + b = 1) : InformationTheory.klDiv (a • μ + b • ν) ρ ≤ ↑a * InformationTheory.klDiv μ ρ + ↑b * InformationTheory.klDiv ν ρ

Convexity of relative entropy. For finite measures and nonnegative weights summing to one, the entropy of their mixture against a fixed finite reference is at most the weighted sum of their entropies. This includes infinite endpoint values and zero weights.

theorem TauCeti.klDiv_smul_add_smul_lt {α : Type u_1} [MeasurableSpace α] {μ ν ρ : MeasureTheory.Measure α} {a b : NNReal} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ρ] (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hμ : InformationTheory.klDiv μ ρ ≠ ⊤) (hν : InformationTheory.klDiv ν ρ ≠ ⊤) (hne : μ ≠ ν) : InformationTheory.klDiv (a • μ + b • ν) ρ < ↑a * InformationTheory.klDiv μ ρ + ↑b * InformationTheory.klDiv ν ρ

Strict convexity of relative entropy on its finite-value domain. Two distinct finite measures with finite entropy against a finite reference have a strict convexity inequality for every mixture with positive weights. The measures need not have equal mass.

@[simp]

theorem TauCeti.klDiv_smul_add_smul_eq_iff {α : Type u_1} [MeasurableSpace α] {μ ν ρ : MeasureTheory.Measure α} {a b : NNReal} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ρ] (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hμ : InformationTheory.klDiv μ ρ ≠ ⊤) (hν : InformationTheory.klDiv ν ρ ≠ ⊤) : InformationTheory.klDiv (a • μ + b • ν) ρ = ↑a * InformationTheory.klDiv μ ρ + ↑b * InformationTheory.klDiv ν ρ ↔ μ = ν

For positive mixture weights and finite endpoint entropies, equality in the entropy convexity inequality holds exactly when the measures are equal.

theorem TauCeti.convex_setOf_isFiniteMeasure_klDiv_ne_top {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ρ] : Convex NNReal {μ : MeasureTheory.Measure α | MeasureTheory.IsFiniteMeasure μ ∧ InformationTheory.klDiv μ ρ ≠ ⊤}

The finite-entropy domain consists of a convex set of finite measures.

theorem TauCeti.strictConvexOn_toReal_klDiv {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ρ] : StrictConvexOn NNReal {μ : MeasureTheory.Measure α | MeasureTheory.IsFiniteMeasure μ ∧ InformationTheory.klDiv μ ρ ≠ ⊤} fun (μ : MeasureTheory.Measure α) => (InformationTheory.klDiv μ ρ).toReal

Relative entropy, read as a real-valued function on its finite-value domain, is strictly convex. This allows the usual StrictConvexOn.eq_of_isMinOn uniqueness theorem to be used.

Quantitative strict convexity

theorem TauCeti.sq_sub_le_mul_klFun_add_klFun_sub {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : (x - y) ^ 2 ≤ 4 * (x + y) * (InformationTheory.klFun x + InformationTheory.klFun y - 2 * InformationTheory.klFun (2⁻¹ * x + 2⁻¹ * y))

Quantitative strict convexity of the entropy integrand. The midpoint convexity defect of InformationTheory.klFun at two nonnegative reals bounds the square of their distance, relative to their sum.

theorem TauCeti.mul_lintegral_enorm_sub_add_two_mul_klDiv_le {α : Type u_1} [MeasurableSpace α] {μ ν ρ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ρ] (t : NNReal) : ↑t * ∫⁻ (x : α), ‖(μ.rnDeriv ρ x).toReal - (ν.rnDeriv ρ x).toReal‖ₑ ∂ρ + 2 * InformationTheory.klDiv (2⁻¹ • μ + 2⁻¹ • ν) ρ ≤ ↑t ^ 2 * (μ Set.univ + ν Set.univ) + InformationTheory.klDiv μ ρ + InformationTheory.klDiv ν ρ

Quantitative strict convexity of relative entropy. For finite measures μ, ν and a finite reference ρ, the convexity defect of relative entropy at the midpoint of μ and ν controls the L¹(ρ) distance of their densities: for every scale t ≥ 0, t * ‖dμ/dρ - dν/dρ‖₁ + 2 * klDiv (μ/2 + ν/2) ρ ≤ t² * (μ(univ) + ν(univ)) + klDiv μ ρ + klDiv ν ρ. Choosing t as the square root of the defect bounds the distance by a multiple of that square root. The inequality holds trivially when an endpoint entropy is infinite.