Kolmogorov–Sinai entropy of a measure-preserving system

Building on the partition-relative entropy ksEntropyPartition hT P = h(α, T) from Oseledets.Entropy.KSEntropy and Oseledets.Entropy.KSEntropyBounds, this file defines the Kolmogorov–Sinai entropy of the system itself, h(T) = sup_α h(α, T), the supremum of the partition-relative entropies over all finite measurable partitions α.

Following the Le Maître notes on the Kolmogorov–Sinai theorem (and the standard Kolmogorov–Sinai definition as recorded in Contractor's The Pesin Entropy Formula, §2, Definition 2.10: "The entropy over all partitions h(T) is the supremum over the entropies for each partition"), the supremum is genuinely over all finite partitions and may be infinite. We therefore value it in EReal, taking the supremum in that complete lattice so the definition is total even when the entropy is +∞.

Concretely the supremum ranges over Fin n-indexed partitions for every n : ℕ; since every finite index type is in bijection with some Fin n and ksEntropyPartition is reindexing invariant, this Fin-indexed family already realizes the full partition supremum, while keeping the index of the iSup a small type.

Main definitions

• Oseledets.Entropy.ksEntropy: the Kolmogorov–Sinai entropy h(T) of a measure-preserving transformation T, the EReal-valued supremum of h(α, T) over all finite partitions α.

Main results

• Oseledets.Entropy.le_ksEntropy: every partition-relative entropy h(α, T) is below h(T).
• Oseledets.Entropy.ksEntropy_nonneg: 0 ≤ h(T), witnessed by the trivial one-cell partition.

References

• François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §1.
• Maryam Contractor, The Pesin Entropy Formula (2023), §2 (standard Kolmogorov–Sinai entropy).

noncomputable def Oseledets.Entropy.ksEntropy {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) : EReal

The Kolmogorov–Sinai entropy of the system h(T): the supremum, taken in EReal, of the partition-relative entropies h(α, T) = ksEntropyPartition hT P over all finite measurable partitions α. The supremum ranges over Fin n-indexed partitions for every n : ℕ; valuing it in the complete lattice EReal makes it total even when the entropy is unbounded (+∞).

Equations

• Oseledets.Entropy.ksEntropy hT = ⨆ (n : ℕ), ⨆ (P : Oseledets.Entropy.MeasurePartition μ (Fin n)), ↑(Oseledets.Entropy.ksEntropyPartition hT P)

theorem Oseledets.Entropy.le_ksEntropy {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) {n : ℕ} (P : MeasurePartition μ (Fin n)) : ↑(ksEntropyPartition hT P) ≤ ksEntropy hT

Every partition-relative Kolmogorov–Sinai entropy h(α, T) is bounded above by the entropy of the system h(T): the defining supremum dominates each of its terms (le_iSup applied to the outer n-indexed and the inner partition-indexed suprema).

def Oseledets.Entropy.trivialPartition {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) : MeasurePartition μ (Fin 1)

The trivial one-cell partition of a probability space: the single cell is the whole space. It is measurable (MeasurableSet.univ), pairwise almost-everywhere disjoint (vacuously, since the index type Fin 1 is a subsingleton), and covers the space (a constant ⋃ over a nonempty index is that constant). It witnesses that the supremum defining ksEntropy ranges over a nonempty family.

Equations

• Oseledets.Entropy.trivialPartition μ = { cells := fun (x : Fin 1) => Set.univ, measurable := ⋯, aedisjoint := ⋯, cover := ⋯ }

theorem Oseledets.Entropy.ksEntropy_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) : 0 ≤ ksEntropy hT

Nonnegativity of the Kolmogorov–Sinai entropy of the system: 0 ≤ h(T). The trivial one-cell partition trivialPartition μ has nonnegative partition-relative entropy (ksEntropyPartition_nonneg), and that entropy is below h(T) by le_ksEntropy; chaining the two EReal inequalities (and EReal.coe_nonneg to lift 0 ≤ h(α, T) to EReal) gives the claim.