Characterizing bounds of the Kolmogorov–Sinai entropy

This file proves the two elementary bounds that pin down the Kolmogorov–Sinai entropy h(α, T) = ksEntropyPartition hT P between 0 and the Shannon entropy H(α) of the generating partition:

• 0 ≤ h(α, T) (ksEntropyPartition_nonneg), and
• h(α, T) ≤ H(α) (ksEntropyPartition_le_entropy).

The first is immediate from the nonnegativity of each averaged iterated-join entropy together with tendsto_ksEntropySeq. The second rests on the linear upper bound ksEntropySeq n ≤ n • H(α) (ksEntropySeq_le_nsmul), obtained by induction from the subadditivity ksEntropySeq_subadditive and the single-step identity ksEntropySeq 1 = H(α) (ksEntropySeq_one); dividing by n ≥ 1 and passing to the Fekete limit yields h(α, T) ≤ H(α).

Main results

• Oseledets.Entropy.ksEntropySeq_one: ksEntropySeq hT P 1 = entropy μ P.cells.
• Oseledets.Entropy.ksEntropySeq_le_nsmul: ksEntropySeq hT P n ≤ n • entropy μ P.cells.
• Oseledets.Entropy.ksEntropyPartition_nonneg: 0 ≤ ksEntropyPartition hT P.
• Oseledets.Entropy.ksEntropyPartition_le_entropy: ksEntropyPartition hT P ≤ entropy μ P.cells.

References

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

@[simp]

theorem Oseledets.Entropy.ksEntropySeq_one {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) : ksEntropySeq hT P 1 = entropy μ P.cells

The single-step iterated-join entropy equals the Shannon entropy of the partition itself: ksEntropySeq hT P 1 = H(α). The 1-fold join ⋁ₖ₌₀⁰ T⁻ᵏ α has cell at f : Fin 1 → ι the single intersection ⋂ₖ T⁻ᵏ (α_{f k}) = T⁰⁻¹(α_{f 0}) = α_{f 0}, so it is α reindexed by the equivalence (Fin 1 → ι) ≃ ι; entropy is invariant under this reindexing.

theorem Oseledets.Entropy.ksEntropySeq_le_nsmul {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (n : ℕ) : ksEntropySeq hT P n ≤ n • entropy μ P.cells

The iterated-join entropy grows at most linearly: ksEntropySeq hT P n ≤ n • H(α). This is the subadditive estimate u n ≤ n • u 1, proved by induction from ksEntropySeq_subadditive, with the single step ksEntropySeq 1 = H(α) substituted via ksEntropySeq_one.

theorem Oseledets.Entropy.ksEntropyPartition_nonneg {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) : 0 ≤ ksEntropyPartition hT P

Nonnegativity of the Kolmogorov–Sinai entropy: 0 ≤ h(α, T). Each averaged iterated-join entropy ksEntropySeq n / n is nonnegative, and the bound passes to the Fekete limit.

theorem Oseledets.Entropy.ksEntropyPartition_le_entropy {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) : ksEntropyPartition hT P ≤ entropy μ P.cells

Upper bound of the Kolmogorov–Sinai entropy by the partition entropy: h(α, T) ≤ H(α). From the linear bound ksEntropySeq n ≤ n • H(α) (ksEntropySeq_le_nsmul), dividing by n ≥ 1 gives ksEntropySeq n / n ≤ H(α) eventually; this passes to the Fekete limit.