Subadditivity of Shannon entropy under joins

This file continues the measure-theoretic foundation for Kolmogorov–Sinai entropy started in Oseledets.Entropy.Partition and Oseledets.Entropy.Join. It establishes the subadditivity of Shannon entropy under the join of two finite measurable partitions, H(α ∨ β) ≤ H(α) + H(β), the analytic heart of the Fekete argument that turns the sequence n ↦ H(⋁ₖ₌₀ⁿ⁻¹ Tᵏα) into the well-defined Kolmogorov–Sinai entropy h(T, α).

Following the Le Maître notes on the Kolmogorov–Sinai theorem, the proof rests on the discrete Gibbs inequality (relative entropy is nonnegative): for a probability vector p and a sub-probability vector q with q i ≠ 0 wherever p i ≠ 0, ∑ᵢ negMulLog (p i) ≤ - ∑ᵢ p i · log (q i). Applying this with p (i,j) = μ(Aᵢ ∩ Bⱼ) and the product q (i,j) = μ(Aᵢ) · μ(Bⱼ) and using the marginal identities μ(Aᵢ) = ∑ⱼ μ(Aᵢ ∩ Bⱼ) and μ(Bⱼ) = ∑ᵢ μ(Aᵢ ∩ Bⱼ) reorganizes the right-hand side into H(α) + H(β).

The scalar Gibbs inequality itself is proved term by term from Real.log_le_sub_one_of_pos, log x ≤ x - 1: where p i > 0 we have q i > 0 and p i · (log (q i) - log (p i)) = p i · log (q i / p i) ≤ q i - p i, and summing the bound over i gives ∑ q - ∑ p ≤ 1 - 1 = 0.

Main results

• Oseledets.Entropy.MeasurePartition.measure_eq_sum_inter: the marginal identity μ A = ∑ j, μ (A ∩ Q.cells j) of a measurable set against a partition.
• Oseledets.Entropy.sum_negMulLog_le: the discrete Gibbs inequality for finite probability and sub-probability vectors that are mutually absolutely continuous on the support of p.
• Oseledets.Entropy.entropy_join_le: subadditivity of Shannon entropy, H(α ∨ β) ≤ H(α) + H(β), for two finite measurable partitions of a probability space.

References

• François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §1.

theorem Oseledets.Entropy.MeasurePartition.measure_eq_sum_inter {α : Type u_1} {κ : Type u_3} [MeasurableSpace α] [Fintype κ] {μ : MeasureTheory.Measure α} (Q : MeasurePartition μ κ) {A : Set α} (hA : MeasurableSet A) : μ A = ∑ j : κ, μ (A ∩ Q.cells j)

Marginal identity. For a measurable set A and a finite measurable partition Q of a measure space, the measure of A is the sum of the measures of its intersections with the cells of Q. The sets A ∩ Q.cells j cover A (since the cells cover the space), are pairwise almost-everywhere disjoint (each is contained in the corresponding cell), and are null-measurable, so finite additivity of μ applies.

theorem Oseledets.Entropy.sum_negMulLog_le {ω : Type u_4} [Fintype ω] (p q : ω → ℝ) (hp : ∀ (i : ω), 0 ≤ p i) (hq : ∀ (i : ω), 0 ≤ q i) (hpsum : ∑ i : ω, p i = 1) (hqsum : ∑ i : ω, q i ≤ 1) (hac : ∀ (i : ω), p i ≠ 0 → q i ≠ 0) : ∑ i : ω, (p i).negMulLog ≤ -∑ i : ω, p i * Real.log (q i)

Discrete Gibbs inequality (nonnegativity of relative entropy). Let p be a probability vector and q a sub-probability vector on a finite index type, with q i ≠ 0 wherever p i ≠ 0. Then ∑ᵢ negMulLog (p i) ≤ - ∑ᵢ p i · log (q i). Equivalently ∑ᵢ p i · log (p i / q i) ≥ 0. The proof bounds each term using log x ≤ x - 1: where p i > 0, p i · (log (q i) - log (p i)) ≤ q i - p i; summing gives ∑ q - ∑ p ≤ 0.

theorem Oseledets.Entropy.entropy_join_le {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurePartition μ ι) (Q : MeasurePartition μ κ) : entropy μ (joinCells P.cells Q.cells) ≤ entropy μ P.cells + entropy μ Q.cells

Subadditivity of Shannon entropy under joins. For two finite measurable partitions P (= α) and Q (= β) of a probability space, the entropy of the join is at most the sum of the entropies: H(α ∨ β) ≤ H(α) + H(β).

This is the discrete Gibbs inequality sum_negMulLog_le applied to the joint distribution p (i,j) = μ(Aᵢ ∩ Bⱼ) and the product distribution q (i,j) = μ(Aᵢ) · μ(Bⱼ). The marginal identities measure_eq_sum_inter show ∑ⱼ p (i,j) = μ(Aᵢ) and ∑ᵢ p (i,j) = μ(Bⱼ), which make ∑ p = 1 and ∑ q = 1, and turn - ∑ p (i,j) · log (μ(Aᵢ) · μ(Bⱼ)) into exactly H(α) + H(β).