The crude Ruelle bound: partition entropy by the log-derivative integral

This module proves the crude Margulis–Ruelle inequality for a smooth self-map T of EuclideanSpace ℝ (Fin d): the Kolmogorov–Sinai partition entropy h(P, T) is bounded by

h(P, T) ≤ d · R, where R is an honest upper bound on the geometric expansion rate

R ≈ ∫ log⁺‖D_x T‖ dμ.

It validates the whole covering pipeline (Oseledets.MeasureTheory.CoveringFromVolume + Oseledets.Entropy.Ruelle.AtomCount) by assembling the scalar arithmetic backbone of the Margulis–Ruelle counting argument into a sorry-free bound, leaving the single genuinely-geometric input — that the partition refines under T^[n] into at most C · exp(n · d · R) non-empty atoms — as an explicit, honest, finite-n hypothesis (hgrow), exactly as Oseledets.margulisRuelle_le_sumPosExp isolates its own geometric input hgeo.

The two layers

1. Oseledets.Entropy.ksEntropyPartition_le_of_atomCount_growth (fully general, sorry-free): the arithmetic backbone. If the non-empty atom count of the refined partition ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P is eventually bounded by C · exp(n · R) with C ≥ 1 and R ≥ 0, then h(P, T) ≤ R. This consumes AtomCountEntropy's ksEntropyPartition_le_limsup_log_atomCount and the elementary limit (1/n)(log C + n R) → R.

2. Oseledets.crudeRuelle_le_log_deriv_rate: the crude Ruelle bound. Specializing the geometric rate to R = d · B, where B is a uniform bound log⁺‖D_x T‖ ≤ B (honest under a globally bounded derivative — see non-compactness below), gives h(P, T) ≤ d · B, conditional on the geometric atom-count growth hypothesis at that rate.

Non-compactness: why a hypothesis is genuinely needed

On the noncompact space EuclideanSpace ℝ (Fin d), Ruelle's inequality has explicit counterexamples (F. Riquelme, Counterexamples to Ruelle's inequality in the noncompact case, Ann. Inst. Fourier 67 (2017) 23–41): suspension-flow-like systems over countable interval exchange transformations have translation-like local behaviour — so the derivative is essentially an isometry, log⁺‖DT‖ ≈ 0 — yet the entropy can be made any prescribed positive value. Thus h(P, T) ≤ d · ∫ log⁺‖DT‖ is false in general here, and the geometric atom-count step (which on a compact manifold follows from a fixed finite cover of bounded distortion) must be supplied as a hypothesis or recovered from extra control on the dynamics (a globally bounded/Lipschitz derivative together with a fixed reference cover, or μ supported on a compact invariant set). We therefore phrase the geometric input as the explicit growth bound hgrow; the scalar reduction around it is unconditional.

Main results

• Oseledets.Entropy.ksEntropyPartition_le_of_atomCount_growth — the arithmetic backbone: atomCount ≤ C · exp(n R) ⇒ h(P, T) ≤ R.
• Oseledets.crudeRuelle_le_log_deriv_rate — the crude Ruelle bound h(P, T) ≤ d · B from the geometric atom-count growth hypothesis at rate d · B (with B the intended uniform log⁺‖DT‖ ≤ B derivative bound).

References

• Maryam Contractor, The Pesin Entropy Formula, UChicago REU 2023, §7 (Margulis–Ruelle inequality, Mañé proof, Lemmas 7.5–7.6).
• Ricardo Mañé, Ergodic theory and differentiable dynamics, Springer 1987, §IV.12 (Lemma 12.5).
• Felipe Riquelme, Counterexamples to Ruelle's inequality in the noncompact case, Ann. Inst. Fourier 67 (2017) 23–41.

theorem Oseledets.Entropy.ksEntropyPartition_le_of_atomCount_growth {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} [Fintype ι] [Nonempty ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) {C R : ℝ} (hC : 1 ≤ C) (hgrow : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(atomCount hT P n) ≤ C * Real.exp (↑n * R)) : ksEntropyPartition hT P ≤ R

Arithmetic backbone of the crude Ruelle bound.

If the number of non-empty atoms of the refined partition ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P is eventually bounded by C · exp(n · R) for some C ≥ 1 and exponential rate R, then the Kolmogorov–Sinai partition entropy is bounded by the rate:

h(P, T) ≤ R.

This is the scalar half of the Margulis–Ruelle counting argument. The atom-count entropy bound ksEntropyPartition_le_limsup_log_atomCount gives h(P, T) ≤ limsupₙ (1/n) · log (atomCount …), and the hypothesis bounds the inner sequence by (1/n) · log (C · exp(n R)) = (log C)/n + R, which tends to R; comparing limsups finishes.

theorem Oseledets.crudeRuelle_le_log_deriv_rate {d : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hT : MeasureTheory.MeasurePreserving T μ μ) {ι : Type u_1} [Fintype ι] [Nonempty ι] (P : Entropy.MeasurePartition μ ι) {B C : ℝ} (hC : 1 ≤ C) (hgrow : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Entropy.atomCount hT P n) ≤ C * Real.exp (↑n * (↑d * B))) : Entropy.ksEntropyPartition hT P ≤ ↑d * B

The crude Ruelle bound.

For a measure-preserving self-map T of EuclideanSpace ℝ (Fin d), a rate B (intended to be a uniform bound log⁺‖D_x T‖ ≤ B on the derivative), and a finite partition P whose n-fold refinement ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P has at most C · exp(n · d · B) non-empty atoms (the geometric atom-counting input, hgrow), the Kolmogorov–Sinai partition entropy is bounded by the positive-part log-derivative rate times the dimension:

h(P, T) ≤ d · B.

Here d · B plays the role of d · ∫ log⁺‖D_x T‖ dμ: the volume of T^[n] '' (atom) grows at most like ‖D(T^[n])‖^d, and operator-norm submultiplicativity together with log⁺‖D(T^[n])‖ ≤ n · B turns the covering count of the image into exp(n · d · B) atoms. Both the uniform-bound interpretation of B and the genuinely geometric step are folded into hgrow (which carries the rate d · B directly); the surrounding reduction is the unconditional Entropy.ksEntropyPartition_le_of_atomCount_growth.

Non-compactness. On the noncompact EuclideanSpace the bare inequality h ≤ d · ∫ log⁺‖DT‖ is false (Riquelme 2017); the cover-growth hypothesis hgrow at rate d · B is the honest extra datum that makes the statement true. See the module docstring.