Documentation

Oseledets.Examples.RuelleDoubling

A non-vacuous instance of the per-partition Ruelle bound: the doubling map #

The abstract per-partition Ruelle inequality h(α, T) ≤ ∑ λᵢ⁺ — entropy relative to one partition α — has as its unconditional arithmetic backbone Oseledets.Entropy.ksEntropyPartition_le_of_atomCount_growth, which isolates the genuinely geometric content as an explicit atom-counting hypothesis and proves everything around it. This module instantiates that content concretely on the classical worked example: the doubling map T : y ↦ 2 • y on the unit circle (Oseledets.doublingMap, Oseledets/Examples/Elementary.lean).

The headline Oseledets.doublingMap_ksEntropyPartition_le_sumPosExp proves the per-partition bound ksEntropyPartition hT P ≤ sumPosExp, i.e. h(α, T) ≤ ∑ λᵢ⁺, for a single partition α — it is not the system Margulis–Ruelle inequality h(T) ≤ ∑ λᵢ⁺. The bridge from the per-partition bound to the system entropy is the Kolmogorov–Sinai identity h(T) = h(α, T) for a generating partition α, which is an un-formalized named input (see below).

For the doubling map the right-hand side equals log 2:

For the binary generating partition the left-hand side is also log 2, so the per-partition bound h(α, T) ≤ log 2 is attained — but that equality is not proved in this file; it is the sibling theorem Oseledets.Examples.Rokhlin.ksEntropyPartition_doublingMap_eq_log_two (h(α, T) = log 2). Cross-referencing that lemma is what backs the "attained" claim with a real proof rather than prose.

What is discharged here, and what stays an honest input #

The atom-count hypothesis hgrow (atomCount ≤ C · 2ⁿ) is automatic for the binary partition: the n-fold refinement of a 2-element partition has at most card(ι)ⁿ = 2ⁿ atoms by the generic bound atomCount ≤ card(ι)ⁿ (the count of formal n-tuples of cells), with no use of any doubling-map-specific geometry. So the natural binary instance exercises no sharp geometric input. The geometric content of hgrow only bites for partitions of cardinality > 2, where card(ι)ⁿ exceeds 2ⁿ and the exact 2-to-1 structure of the doubling map (a partition into intervals refines under T^[n] into ≈ 2ⁿ atoms, not card(ι)ⁿ) is what pins the rate down. The hypothesis has exactly the status the Mañé/Katok count carries in Oseledets.Entropy.Ruelle.Crude, here with the rate log 2 matching the true exponent.

The remaining bridge to a fully unconditional h(T) ≤ log 2 over the system entropy is the Kolmogorov–Sinai theorem h(T) = h(α, T) for a generating partition α (Le Maître's notes, §1), multi-month-scale ergodic infrastructure not present in Mathlib, hence deliberately left as the named input.

Main results #

References #

The positive-exponent sum of the doubling-map cocycle is log 2 #

source
theorem Oseledets.doublingMap_exponents_eq_log_two (i : Fin (Fintype.card (Fin 1))) :
exponents ergodic_doublingMap ⋯ ⋯ ⋯ ⋯ i = Real.log 2

The single Lyapunov exponent of the doubling-map constant cocycle (generator M = !![2], indexed by Fin (Fintype.card (Fin 1)) = Fin 1) is log 2.

This is Oseledets.doublingMap_topExponent_eq_log_two read off the only spectrum index: the top exponent exponents … ⟨0, _⟩ is the single exponent, and a subsingleton index forces every index to that value.

source
theorem Oseledets.doublingMap_sumPosExp_eq_log_two :
sumPosExp ergodic_doublingMap ⋯ ⋯ ⋯ ⋯ = Real.log 2

Doubling map: the sum of the strictly positive Lyapunov exponents is log 2.

The right-hand side of the Margulis–Ruelle inequality for the doubling-map constant cocycle (generator M = !![2]) is log 2: the spectrum has a single exponent log 2 > 0, so the positive-exponent sum is that one term. Every hypothesis (invertibility, measurability, and the two log-integrability conditions) is discharged from the constant-cocycle API, so this computation is unconditional.

The non-vacuous per-partition Ruelle inequality for the doubling map #

source
theorem Oseledets.doublingMap_ksEntropyPartition_le_sumPosExp {ι : Type u_1} [Fintype ι] [Nonempty ι] (P : Entropy.MeasurePartition MeasureTheory.volume ι) {C : ℝ} (hC : 1 ≤ C) (hgrow : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Entropy.atomCount ⋯ P n) ≤ C * Real.exp (↑n * Real.log 2)) :
Entropy.ksEntropyPartition ⋯ P ≤ sumPosExp ergodic_doublingMap ⋯ ⋯ ⋯ ⋯

The per-partition Ruelle bound for the doubling map.

For any finite measurable partition P of the unit circle whose n-fold refinement ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P under the doubling map has eventually at most C · 2ⁿ non-empty atoms (hgrow, with C ≥ 1), the Kolmogorov–Sinai entropy relative to that single partition is bounded by the sum of the strictly positive Lyapunov exponents of the (constant) derivative cocycle:

h(α, T) ≤ ∑ λᵢ⁺ = log 2.

This is the per-partition Ruelle bound h(α, T) ≤ ∑ λᵢ⁺, not the system inequality h(T) ≤ ∑ λᵢ⁺ (which additionally needs the Kolmogorov–Sinai identity h(T) = h(α, T) for a generating partition — an un-formalized named input; see the module docstring). The right-hand side is the computed exponent sum log 2 (doublingMap_sumPosExp_eq_log_two), not an abstract constant.

The bound is attained for the binary generating partition, where h(α, T) = log 2 — but that equality is proved in the sibling theorem Oseledets.Examples.Rokhlin.ksEntropyPartition_doublingMap_eq_log_two, not here.

The atom-count growth hgrow is automatic for the binary partition (its n-refinement has at most card(ι)ⁿ = 2ⁿ atoms by the generic tuple bound, no doubling-map geometry); the geometric content of hgrow only bites for partitions of cardinality > 2, where the exact 2-to-1 structure of the doubling map (≈ 2ⁿ interval atoms, not card(ι)ⁿ) is what pins the rate log 2 down (note 2ⁿ = exp(n · log 2)). The reduction itself is the unconditional arithmetic backbone Oseledets.Entropy.ksEntropyPartition_le_of_atomCount_growth.