Dynamical subadditivity of the Kolmogorov–Sinai entropy under joins

For a measure-preserving transformation T and two finite measurable partitions α and β, the partition-relative Kolmogorov–Sinai entropy is subadditive under the join: h(α ∨ β, T) ≤ h(α, T) + h(β, T).

This is the dynamical refinement of the static join subadditivity H(α ∨ β) ≤ H(α) + H(β) (entropy_join_le) into the long-run entropy rate. The mechanism is a structural cell identity: the n-fold dynamical join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ(α ∨ β) of the join is, cell by cell, the static join of the n-fold dynamical join of α with the n-fold dynamical join of β. Indeed for an index f : Fin n → ι × κ, ⋂ₖ T⁻ᵏ((α ∨ β)_{f k}) = ⋂ₖ T⁻ᵏ(α_{(f k).1} ∩ β_{(f k).2}) = (⋂ₖ T⁻ᵏ α_{(f k).1}) ∩ (⋂ₖ T⁻ᵏ β_{(f k).2}), because preimages and finite intersections commute. Reindexing the product index type Fin n → ι × κ by Equiv.arrowProdEquivProdArrow (so f ↦ (g, h) with g k = (f k).1, h k = (f k).2) identifies the n-fold join entropy of α ∨ β with the static join entropy of the two n-fold joins; entropy_join_le then bounds it by ksEntropySeq α n + ksEntropySeq β n. Dividing by n and passing both sides to the Fekete limit (tendsto_ksEntropySeq, le_of_tendsto_of_tendsto', with the sum limit from Tendsto.add) yields the claim.

Main definitions

• Oseledets.Entropy.joinPartition: the join (common refinement) α ∨ β of two finite measurable partitions, as a MeasurePartition μ (ι × κ) with cells joinCells α.cells β.cells.

Main results

• Oseledets.Entropy.ksEntropySeq_join_le: ksEntropySeq (α ∨ β) n ≤ ksEntropySeq α n + ksEntropySeq β n, the per-n cell-level subadditivity.
• Oseledets.Entropy.ksEntropyPartition_join_le: h(α ∨ β, T) ≤ h(α, T) + h(β, T), the dynamical subadditivity of the Kolmogorov–Sinai entropy under joins.

References

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

def Oseledets.Entropy.joinPartition {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} (P : MeasurePartition μ ι) (Q : MeasurePartition μ κ) : MeasurePartition μ (ι × κ)

The join partition α ∨ β, the common refinement of two finite measurable partitions P (= α) and Q (= β) of a probability space, as a MeasurePartition μ (ι × κ) with cell at (i, j) the intersection Aᵢ ∩ Bⱼ (joinCells P.cells Q.cells). Each cell is measurable as the intersection of two measurable cells; the cells are pairwise almost-everywhere disjoint because two distinct pairs (i, j) ≠ (i', j') differ in some coordinate, where the corresponding P- or Q-cells are a.e. disjoint and the cell is contained in that coordinate's cell; and the cells cover the space since ⋃_{i,j} Aᵢ ∩ Bⱼ = (⋃ᵢ Aᵢ) ∩ (⋃ⱼ Bⱼ) = univ ∩ univ.

Equations

• Oseledets.Entropy.joinPartition P Q = { cells := Oseledets.Entropy.joinCells P.cells Q.cells, measurable := ⋯, aedisjoint := ⋯, cover := ⋯ }

@[simp]

theorem Oseledets.Entropy.joinPartition_cells {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} (P : MeasurePartition μ ι) (Q : MeasurePartition μ κ) : (joinPartition P Q).cells = joinCells P.cells Q.cells

theorem Oseledets.Entropy.ksJoinCells_joinCells {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (s : ι → Set α) (t : κ → Set α) (T : α → α) (n : ℕ) (f : Fin n → ι × κ) : ksJoinCells (joinCells s t) T n f = (ksJoinCells s T n fun (k : Fin n) => (f k).1) ∩ ksJoinCells t T n fun (k : Fin n) => (f k).2

Structural cell identity for the iterated join of a join. The cell of the n-fold dynamical join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ(α ∨ β) at an index f : Fin n → ι × κ is the intersection of the cell of the n-fold join of α at the first-coordinate index k ↦ (f k).1 with the cell of the n-fold join of β at the second-coordinate index k ↦ (f k).2. This holds because preimages and finite intersections commute: ⋂ₖ T⁻ᵏ(α_{(f k).1} ∩ β_{(f k).2}) = (⋂ₖ T⁻ᵏ α_{(f k).1}) ∩ (⋂ₖ T⁻ᵏ β_{(f k).2}).

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

Per-n cell-level subadditivity. The n-fold dynamical-join entropy of the join α ∨ β is at most the sum of the n-fold dynamical-join entropies of α and β: H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ(α ∨ β)) ≤ H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α) + H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ β).

Reindexing the product index Fin n → ι × κ by Equiv.arrowProdEquivProdArrow and using the cell identity ksJoinCells_joinCells, the (α ∨ β)-join entropy equals the static join entropy of the two n-fold joins; entropy_join_le then bounds it by the sum.

theorem Oseledets.Entropy.ksEntropyPartition_join_le {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (Q : MeasurePartition μ κ) : ksEntropyPartition hT (joinPartition P Q) ≤ ksEntropyPartition hT P + ksEntropyPartition hT Q

Dynamical subadditivity of the Kolmogorov–Sinai entropy under joins: h(α ∨ β, T) ≤ h(α, T) + h(β, T).

The per-n bound ksEntropySeq_join_le divided by n reads ksEntropySeq (α ∨ β) n / n ≤ ksEntropySeq α n / n + ksEntropySeq β n / n. Each averaged sequence converges to its Kolmogorov–Sinai entropy by tendsto_ksEntropySeq, so the right-hand side converges to h(α, T) + h(β, T) (Tendsto.add); passing the pointwise inequality to the limits (le_of_tendsto_of_tendsto') gives the claim.