Kolmogorov–Sinai entropy via the Fekete limit

This file completes the measure-theoretic foundation for Kolmogorov–Sinai entropy started in Oseledets.Entropy.Partition, Oseledets.Entropy.Join, Oseledets.Entropy.Subadditive, Oseledets.Entropy.Subadditive2, and Oseledets.Entropy.Fekete. It defines the entropy h(α, T) of a measure-preserving transformation T relative to a finite measurable partition α as the Fekete limit of the iterated-join entropy sequence.

Following the Le Maître notes on the Kolmogorov–Sinai theorem, the iterated join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α is realized here with a Fin-indexed cell family, where the cell at an index f : Fin n → ι is the intersection ⋂ₖ T⁻ᵏ (α_{f k}). This flat Fin-indexing is what makes the n + m subadditivity close: splitting Fin (n + m) ≃ Fin n ⊕ Fin m exhibits the (n + m)-fold join, up to a reindexing of cells by Fin.appendEquiv, as the ordinary join of the n-fold join with the Tⁿ-pullback of the m-fold join. Combined with the join subadditivity entropy_join_le and the pullback invariance entropy_pullback, this gives ksEntropySeq (n + m) ≤ ksEntropySeq n + ksEntropySeq m, so the sequence is Subadditive, and Subadditive.tendsto_lim (Fekete's lemma) produces the limit h(α, T), with the boundedness hypothesis discharged from nonnegativity.

Main definitions

• Oseledets.Entropy.ksJoin: the flat Fin n-indexed iterated join, a measurable partition.
• Oseledets.Entropy.ksEntropySeq: the entropy sequence n ↦ H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α).
• Oseledets.Entropy.ksEntropyPartition: the Kolmogorov–Sinai entropy h(α, T), the Fekete limit.

Main results

• Oseledets.Entropy.ksEntropySeq_subadditive: ksEntropySeq (n + m) ≤ ksEntropySeq n + ksEntropySeq m.
• Oseledets.Entropy.ksSubadditive: the sequence is a Subadditive sequence.
• Oseledets.Entropy.tendsto_ksEntropySeq: n ↦ ksEntropySeq n / n tends to ksEntropyPartition.

References

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

def Oseledets.Entropy.ksJoinCells {α : Type u_1} {ι : Type u_2} (cells : ι → Set α) (T : α → α) (n : ℕ) (f : Fin n → ι) : Set α

The cell family of the flat Fin n-indexed iterated join: the cell at f : Fin n → ι is the intersection ⋂ₖ T⁻ᵏ (α_{f k}) of the pullbacks of the chosen α-cells along the first n iterates of T. For n = 0 the index type Fin 0 → ι has a single element and the empty intersection is the whole space, so the join is the trivial one-cell partition.

Equations

• Oseledets.Entropy.ksJoinCells cells T n f = ⋂ (k : Fin n), T^[↑k] ⁻¹' cells (f k)

@[simp]

theorem Oseledets.Entropy.ksJoinCells_apply {α : Type u_1} {ι : Type u_2} (cells : ι → Set α) (T : α → α) (n : ℕ) (f : Fin n → ι) : ksJoinCells cells T n f = ⋂ (k : Fin n), T^[↑k] ⁻¹' cells (f k)

noncomputable def Oseledets.Entropy.ksJoin {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (n : ℕ) : MeasurePartition μ (Fin n → ι)

The flat iterated join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α, indexed by Fin n → ι: the finite measurable partition whose cell at f is ⋂ₖ T⁻ᵏ (α_{f k}). Each cell is a finite intersection of preimages of measurable sets under the measurable iterates Tᵏ; two distinct indices differ at some k, where the corresponding α-cells are almost-everywhere disjoint and Tᵏ preserves the measure, so the cells are pairwise almost-everywhere disjoint; and the cells cover the space because for each point one can choose, at every coordinate k, the α-cell that Tᵏ x lies in.

Equations

• Oseledets.Entropy.ksJoin hT P n = { cells := Oseledets.Entropy.ksJoinCells P.cells T n, measurable := ⋯, aedisjoint := ⋯, cover := ⋯ }

@[simp]

theorem Oseledets.Entropy.ksJoin_cells {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (n : ℕ) : (ksJoin hT P n).cells = ksJoinCells P.cells T n

noncomputable def Oseledets.Entropy.ksEntropySeq {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (n : ℕ) : ℝ

The iterated-join entropy sequence n ↦ H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α) for the flat Fin-indexed join. Its Fekete limit is the Kolmogorov–Sinai entropy h(α, T).

Equations

• Oseledets.Entropy.ksEntropySeq hT P n = Oseledets.Entropy.entropy μ (Oseledets.Entropy.ksJoin hT P n).cells

@[simp]

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

The flat n = 0 join is the trivial one-cell partition, of entropy 0: its only cell (the empty intersection) is the whole space, which has measure 1, and negMulLog 1 = 0.

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

The iterated-join entropy is nonnegative for a probability measure.

theorem Oseledets.Entropy.entropy_reindex {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {β : Type u_3} [Fintype β] (μ : MeasureTheory.Measure α) (e : ι ≃ β) (s : β → Set α) : (entropy μ fun (i : ι) => s (e i)) = entropy μ s

Reindexing invariance of Shannon entropy. Precomposing the cell family with an equivalence of index types leaves the entropy unchanged, since it merely permutes the summands.

theorem Oseledets.Entropy.ksJoinCells_append {α : Type u_1} {ι : Type u_2} (cells : ι → Set α) (T : α → α) (n m : ℕ) (a : Fin n → ι) (b : Fin m → ι) : ksJoinCells cells T (n + m) (Fin.append a b) = ksJoinCells cells T n a ∩ T^[n] ⁻¹' ksJoinCells cells T m b

Structural cell identity for the flat iterated join. Under the append equivalence Fin.appendEquiv n m : (Fin n → ι) × (Fin m → ι) ≃ (Fin (n + m) → ι), the cell of the (n + m)-fold join at Fin.append a b is the intersection of the cell of the n-fold join at a with the Tⁿ-pullback of the cell of the m-fold join at b. This is the join–pullback factorization underlying the subadditivity.

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

Subadditivity of the iterated-join entropy (the Fekete inequality): H(⋁ₖ₌₀ⁿ⁺ᵐ⁻¹ T⁻ᵏ α) ≤ H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α) + H(⋁ₖ₌₀ᵐ⁻¹ T⁻ᵏ α). Reindexing the (n + m)-fold join by Fin.appendEquiv exhibits it as the join of the n-fold join with the Tⁿ-pullback of the m-fold join (ksJoinCells_append); the join subadditivity entropy_join_le then bounds it by the sum of the two entropies, and the pullback invariance entropy_pullback identifies the second summand as the m-fold join entropy (Tⁿ is measure-preserving by hT.iterate n).

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

The iterated-join entropy sequence is a Subadditive sequence in the sense of Fekete's lemma: u (k + l) ≤ u k + u l. This is ksEntropySeq_subadditive repackaged.

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

The Kolmogorov–Sinai entropy h(α, T) of a measure-preserving transformation T relative to a finite measurable partition α, defined as the Fekete limit limₙ (1 / n) · H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α) of the subadditive iterated-join entropy sequence.

Equations

• Oseledets.Entropy.ksEntropyPartition hT P = ⋯.lim

theorem Oseledets.Entropy.tendsto_ksEntropySeq {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) : Filter.Tendsto (fun (n : ℕ) => ksEntropySeq hT P n / ↑n) Filter.atTop (nhds (ksEntropyPartition hT P))

Fekete convergence to the Kolmogorov–Sinai entropy. The averaged iterated-join entropies (1 / n) · H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α) converge to h(α, T). The boundedness-below hypothesis of Fekete's lemma Subadditive.tendsto_lim is discharged from the nonnegativity of the entropies: each ksEntropySeq n / n is at least 0, so the range is bounded below by 0.