Partition entropy bounded by the growth rate of the non-empty atom count

This file bounds the dynamical (Kolmogorov–Sinai) partition entropy h(α, T) of a measure-preserving transformation T relative to a finite measurable partition α = P by the exponential growth rate of the number of non-empty atoms of the refined partition ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P. Concretely,

h(α, T) ≤ limsupₙ (1 / n) · log (#{non-empty atoms of ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P}).

This is the entropy-bookkeeping half of the Margulis–Ruelle inequality (Le Maître's notes, the Mañé proof in Contractor's REU notes): the geometric content of that inequality is to count how many atoms of a small partition survive under T^[n], and this file packages the abstract step that turns such an atom count into a bound on h(α, T). It uses only the present entropy API:

• the Jensen bound entropy_le_log_card (Oseledets.Entropy.Partition), which gives H(α) ≤ log #α, here strengthened to count only the non-empty cells (the empty ones, of measure zero, contribute negMulLog 0 = 0 to the entropy), and
• the Fekete limit ksEntropyPartition = limₙ (1 / n) · H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P) (Oseledets.Entropy.KSEntropy).

Combining H(⋁ₖ₌₀ⁿ⁻¹) ≤ log (#non-empty atoms) with the convergence of the averaged sequence and passing to the limsup gives the displayed bound.

Main definitions

• Oseledets.Entropy.atomCount: the number of non-empty atoms of the flat n-fold join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P, as a ℕ (the cardinality of the Finset of indices f : Fin n → ι whose cell is non-empty).

Main results

• Oseledets.Entropy.entropy_le_log_card_filter: a Jensen entropy bound counting only the cells outside of which the family is μ-null.
• Oseledets.Entropy.entropy_le_log_atomCount: the single-n bound H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P) ≤ log (atomCount …).
• Oseledets.Entropy.ksEntropyPartition_le_limsup_log_atomCount: the dynamical bound h(α, T) ≤ limsupₙ (1 / n) · log (atomCount …).

References

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

theorem Oseledets.Entropy.entropy_le_log_card_filter {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] (μ : MeasureTheory.Measure α) (s : ι → Set α) (S : Finset ι) (hS : S.Nonempty) (hnull : ∀ i ∉ S, μ (s i) = 0) (hsum : ∑ i : ι, (μ (s i)).toReal = 1) : entropy μ s ≤ Real.log ↑S.card

Jensen entropy bound counting only the supported cells. If the cell measures of a finite family s : ι → Set α sum to 1 and s i is μ-null for every index outside a non-empty Finset S, then the Shannon entropy is bounded by log #S. This sharpens entropy_le_log_card: cells of measure zero contribute negMulLog 0 = 0 to the entropy, so only the supported cells count. The proof is Jensen's inequality for the concave negMulLog with equal weights (#S)⁻¹ over S.

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

The non-empty atom count of the flat n-fold join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P: the number of indices f : Fin n → ι whose atom ⋂ₖ T⁻ᵏ (P_{f k}) is non-empty, as a natural number. This is the combinatorial quantity whose exponential growth rate bounds the dynamical partition entropy.

Equations

• Oseledets.Entropy.atomCount hT P n = {f : Fin n → ι | ((Oseledets.Entropy.ksJoin hT P n).cells f).Nonempty}.card

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

The non-empty atom count is positive: the cells cover the whole (probability) space, so at least one of them is non-empty.

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

Single-n atom-count bound. The Shannon entropy of the flat n-fold join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P is at most the logarithm of its non-empty atom count. The empty atoms have measure zero, so entropy_le_log_card_filter (counting only the non-empty cells) applies, with the cell measures summing to 1 because ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P is a partition of a probability space.

theorem Oseledets.Entropy.ksEntropyPartition_le_limsup_log_atomCount {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] [Nonempty ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) : ksEntropyPartition hT P ≤ Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ↑(atomCount hT P n)) Filter.atTop

Dynamical atom-count entropy bound. The Kolmogorov–Sinai partition entropy h(α, T) is bounded by the exponential growth rate of the number of non-empty atoms of the refined partition ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P:

h(α, T) ≤ limsupₙ (1 / n) · log (atomCount …).

The averaged iterated-join entropies (1 / n) · H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P) converge to h(α, T) (tendsto_ksEntropySeq), so h(α, T) is their limsup; the per-n bound H(⋁ₖ₌₀ⁿ⁻¹) ≤ log (atomCount …) (entropy_le_log_atomCount) divides through by n and is then compared limsup-to-limsup. The required boundedness is supplied by the convergence of the averaged entropies (giving coboundedness of the left side) and by the uniform bound (1 / n) · log (atomCount …) ≤ log #ι — the atom count never exceeds the total number of indices #(Fin n → ι) = (#ι)ⁿ.