Le Maître's inequality (7): the static-conditional-entropy correction

For a measure-preserving transformation T and two finite measurable partitions α = P and β = P', the Kolmogorov–Sinai entropies obey the Le Maître inequality (7) h(α, T) ≤ h(β, T) + H(α | σ(β)), where H(α | σ(β)) is the static conditional Shannon entropy of α given the σ-algebra σ(β) generated by the cells of β. This is the first half of the Kolmogorov–Sinai theorem (the bound that drives h(T) = h(β, T) when β is generating) and a building block for the product-entropy upper bound h(T × id) ≤ h(T) (Walters, Theorem 4.23).

The dynamical statement reduces to a per-n bound. Writing A_n = ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α and B_n = ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ β for the flat Fin n-indexed iterated joins:

• refinement + chain rule (entropy_le_entropy_join, the chain rule, and the σ-algebra bridge condEntropyGivenPartition_eq_condEntropy_generated): H(A_n) ≤ H(A_n ∨ B_n) = H(B_n) + H(A_n | σ(B_n));
• finite conditional subadditivity (condEntropy_ksJoin_le_sum): H(A_n | σ(B_n)) ≤ ∑ₖ<ₙ H(T⁻ᵏα | σ(B_n));
• moving-conditioning collapse (condEntropy_mono_of_le, then the invariance condEntropy_comap_pullback): each summand is at most H(α | σ(β)), because σ(T⁻ᵏβ) = comap (T^[k]) σ(β) ⊆ σ(B_n) (for k < n) and conditioning on the bigger σ-algebra decreases entropy, while H(T⁻ᵏα | comap (T^[k]) σ(β)) = H(α | σ(β)).

Together these give H(A_n) ≤ H(B_n) + n · H(α | σ(β)); dividing by n and passing both Fekete limits (tendsto_ksEntropySeq) yields the dynamical inequality.

Main results

• Oseledets.Entropy.condEntropy_reindex: invariance of condEntropy under reindexing the cell family by an equivalence of finite index types.
• Oseledets.Entropy.entropy_joinCells_comm: symmetry H(α ∨ β) = H(β ∨ α) of the static join entropy.
• Oseledets.Entropy.condEntropy_ksJoin_le_sum: finite conditional subadditivity of the iterated-join entropy, H(A_n | 𝒞) ≤ ∑ₖ<ₙ H(T⁻ᵏα | 𝒞), for an arbitrary fixed sub-σ-algebra 𝒞.
• Oseledets.Entropy.ksEntropySeq_le_add_condEntropy: the per-n bound H(A_n) ≤ H(B_n) + n · H(α | σ(β)).
• Oseledets.Entropy.ksEntropyPartition_le_add_condEntropy: Le Maître's inequality (7), h(α, T) ≤ h(β, T) + H(α | σ(β)).

References

• François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §1–2, inequality (7).
• Peter Walters, An Introduction to Ergodic Theory, Springer GTM 79, Chapter 4.

theorem Oseledets.Entropy.condEntropy_reindex {α : Type u_1} [mα : MeasurableSpace α] [StandardBorelSpace α] {β : Type u_4} {γ : Type u_5} [Fintype β] [Fintype γ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (𝒜 : MeasurableSpace α) (e : β ≃ γ) (s : γ → Set α) : (condEntropy μ 𝒜 fun (i : β) => s (e i)) = condEntropy μ 𝒜 s

Reindexing invariance of conditional Shannon entropy. Precomposing the cell family with an equivalence e : β ≃ γ of finite index types leaves the conditional entropy unchanged, since it merely permutes the summands of the pointwise entropy integrand.

theorem Oseledets.Entropy.entropy_joinCells_comm {α : Type u_1} [mα : MeasurableSpace α] {β : Type u_4} {γ : Type u_5} [Fintype β] [Fintype γ] {μ : MeasureTheory.Measure α} (s : β → Set α) (t : γ → Set α) : entropy μ (joinCells s t) = entropy μ (joinCells t s)

Symmetry of the static join entropy: H(α ∨ β) = H(β ∨ α). The join cell families (i, j) ↦ sᵢ ∩ tⱼ and (j, i) ↦ tⱼ ∩ sᵢ agree after swapping the product index and using commutativity of intersection, so they have equal Shannon entropy.

theorem Oseledets.Entropy.condEntropy_ksJoin_le_sum {α : Type u_1} {ι : Type u_2} {𝒞 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (h𝒞 : 𝒞 ≤ mα) (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (n : ℕ) : condEntropy μ 𝒞 (ksJoin hT P n).cells ≤ ∑ k : Fin n, condEntropy μ 𝒞 (MeasurePartition.pullback ⋯ P).cells

Finite conditional subadditivity of the iterated-join entropy. For an arbitrary fixed sub-σ-algebra 𝒞 ≤ mα, the conditional entropy of the n-fold join is at most the sum of the conditional entropies of the n single coordinates: H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α | 𝒞) ≤ ∑ₖ<ₙ H(T⁻ᵏ α | 𝒞).

Induction on n: the n = 0 join is trivial (entropy 0), and the inductive step front-peels the last coordinate via condEntropy_ksJoin_append_le (with block lengths n and 1), identifying the length-1 block T⁻ⁿ(⋁ₖ₌₀⁰ T⁻ᵏα) with the single pullback T⁻ⁿα (reindexing (Fin 1 → ι) ≃ ι via condEntropy_reindex); the induction hypothesis bounds the remaining n-fold join.

theorem Oseledets.Entropy.ksEntropySeq_le_add_condEntropy {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (P' : MeasurePartition μ κ) (n : ℕ) : ksEntropySeq hT P n ≤ ksEntropySeq hT P' n + ↑n * condEntropy μ (generatedSigmaAlgebra μ P') P.cells

Per-n Le Maître bound. For finite measurable partitions α = P and β = P', H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α) ≤ H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ β) + n · H(α | σ(β)), where H(α | σ(β)) = condEntropy μ (generatedSigmaAlgebra μ β) α.

Refinement (entropy_le_entropy_join), the entropy chain rule and the σ-algebra bridge (condEntropyGivenPartition_eq_condEntropy_generated) give H(A_n) ≤ H(B_n) + H(A_n | σ(B_n)); finite conditional subadditivity (condEntropy_ksJoin_le_sum) splits the last term into n single-coordinate conditional entropies, each of which collapses to H(α | σ(β)) by conditioning monotonicity (condEntropy_mono_of_le) against comap (T^[k]) σ(β) ⊆ σ(B_n) (for k < n) followed by the joint-pullback invariance (condEntropy_comap_pullback).

theorem Oseledets.Entropy.ksEntropyPartition_le_add_condEntropy {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (P' : MeasurePartition μ κ) : ksEntropyPartition hT P ≤ ksEntropyPartition hT P' + condEntropy μ (generatedSigmaAlgebra μ P') P.cells

Le Maître's inequality (7) (static-conditional-entropy correction). For a measure-preserving transformation T and finite measurable partitions α = P and β = P', the Kolmogorov–Sinai entropy of α is bounded by that of β plus the static conditional Shannon entropy of α given the σ-algebra σ(β) generated by β: h(α, T) ≤ h(β, T) + H(α | σ(β)).

Divide the per-n bound ksEntropySeq_le_add_condEntropy by n, reading H(A_n)/n ≤ H(B_n)/n + H(α | σ(β)), then pass both averaged iterated-join entropies to their Fekete limits (tendsto_ksEntropySeq); le_of_tendsto_of_tendsto' transfers the inequality to the limits.