The sharp Ruelle counting bound: orbit iteration of the local covering

This module assembles the orbit-iteration half of the sharp Margulis–Ruelle inequality h(P, T) ≤ ∑ λᵢ⁺ for a smooth ergodic self-map T of EuclideanSpace ℝ (Fin d). The crude bound of Oseledets.Entropy.Ruelle.Crude controls the partition entropy by the dimension times the uniform log-derivative bound, d · B; this module sharpens the geometric rate from d · B to the genuine positive-exponent sum sumPosExp = ∑_{λᵢ > 0} λᵢ, by counting the image of an ε-ball under the n-fold iterate T^[n] via the positive-part singular-value product of the derivative cocycle.

The per-orbit volume factor

The local volume-expansion factor of the differential D_x(T^[n]) — counting only the expanding directions — is the positive-part singular-value product

volProd T n x = ∏_{i < d} max 1 σᵢ(D_x(T^[n])),

where σᵢ(D_x(T^[n])) are the singular values of the cocycle iterate cocycle (derivativeCocycle T) T n x (the chain-rule cocycle, chainRule_cocycle). Its logarithm is ∑_{i} log⁺ σᵢ (Oseledets.Entropy.sum_posLog_singularValues_toEuclideanLin_eq), the finite-n incarnation of ∑ λᵢ⁺.

The two layers

1. The orbit growth rate (tendsto_log_volProd, sorry-free). For μ-a.e. x, (1/n) · log (volProd T n x) → sumPosExp. This is the genuinely new orbit-iteration content: each per-singular-value term (1/n) log⁺ σᵢ = max 0 ((1/n) log σᵢ) converges to max 0 (exponents i) (continuity of max 0 · composed with the per-exponent limit Oseledets.exponents_tendsto_log_singularValue), and the finite sum of these limits is exactly ∑ᵢ max 0 (exponents i) = sumPosExp (the positive part of an antitone spectrum, summed with multiplicity). No extra Furstenberg–Kesten integrability is needed: the rate rides on the already-established per-exponent singular-value limits.

2. The local covering count (coveringCount_image_ball_le_volProd, proved in-tree). The genuinely geometric per-step input — the image L '' (ball x ε) of an ε-ball under a linear map L is coverable by at most 6^d · ∏ᵢ max(1, σᵢ(L)) balls of radius ε — is fully proved in-tree in the sibling module Oseledets.Entropy.Ruelle.SharpCovering (via a constructive SVD ellipsoid domination + determinant volume bound). Specialised to the orbit differential L = D_x(T^[n]) (Oseledets.chainRule_cocycle) it gives exactly the per-orbit volProd count. The honest mathematical caveat is the non-compactness distortion regime (hgeo below, Riquelme 2017), not the covering count itself.

Feeding the orbit rate (layer 1) into the abstract atom-count reduction Oseledets.Entropy.ksEntropyPartition_le_of_atomCount_growth (Oseledets.Entropy.Ruelle.Crude) turns the per-step covering count into the per-partition bound h(P, T) ≤ sumPosExp, which discharges the hgeo / hcount hypothesis of Oseledets.margulisRuelle_le_sumPosExp.

Non-compactness

We carry the same honest non-compactness data as Oseledets.Entropy.Ruelle.Crude (a uniform derivative / bounded-distortion regime — on the noncompact EuclideanSpace the bare inequality h ≤ ∑ λᵢ⁺ is false, Riquelme 2017). Here the geometric input is distilled to the single explicit hypothesis hatom: there is a base point x of the full-measure orbit-rate set at which the non-empty atom count of the refined partition is eventually bounded by C · volProd T n x. This is exactly the output of the Mañé/Katok covering–distortion counting argument; the surrounding orbit reduction is unconditional.

Main results

• Oseledets.volProd — the per-orbit positive-part singular-value product ∏_{i<d} max 1 σᵢ(D(T^[n])).
• Oseledets.one_le_volProd — the volume factor is ≥ 1.
• Oseledets.log_volProd_eq_sum_posLog — log (volProd …) = ∑_{i<d} log⁺ σᵢ.
• Oseledets.tendsto_log_volProd — the orbit growth rate (1/n) log (volProd …) → sumPosExp, a.e. (sorry-free).
• Oseledets.coveringCount_image_ball_le_volProd — the sharp local covering count, proved in-tree in the sibling Oseledets.Entropy.Ruelle.SharpCovering.
• Oseledets.ksEntropyPartition_le_sumPosExp_of_atomVolProd — the orbit assembly: a base-point volProd atom-count bound yields h(P, T) ≤ sumPosExp.
• Oseledets.margulisRuelle_sharp_of_atomVolProd — the sharp Margulis–Ruelle inequality h(T) ≤ ∑ λᵢ⁺, conditional on the (honest, distilled) geometric atom-count input.

References

• Maryam Contractor, The Pesin Entropy Formula, UChicago REU 2023, §7.
• Ricardo Mañé, Ergodic theory and differentiable dynamics, Springer 1987, §IV.12.
• D. Ruelle, An inequality for the entropy of differentiable maps, Bol. Soc. Bras. Mat. 9 (1978) 83–87.
• Felipe Riquelme, Counterexamples to Ruelle's inequality in the noncompact case, Ann. Inst. Fourier 67 (2017) 23–41.

noncomputable def Oseledets.volProd {d : ℕ} (T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (n : ℕ) (x : EuclideanSpace ℝ (Fin d)) : ℝ

The per-orbit positive-part singular-value product. For a self-map T of EuclideanSpace ℝ (Fin d), volProd T n x is the product over the d singular-value indices of max 1 σᵢ(D_x(T^[n])), where σᵢ are the singular values of the chain-rule cocycle iterate cocycle (derivativeCocycle T) T n x. It is the local volume-expansion factor of D_x(T^[n]) restricted to its expanding directions; its log is ∑ᵢ log⁺ σᵢ, the finite-n form of ∑ λᵢ⁺.

Equations

• Oseledets.volProd T n x = ∏ i ∈ Finset.range d, max 1 ((Matrix.toEuclideanLin (Oseledets.cocycle (Oseledets.derivativeCocycle T) T n x)).singularValues i)

theorem Oseledets.one_le_volProd {d : ℕ} (T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (n : ℕ) (x : EuclideanSpace ℝ (Fin d)) : 1 ≤ volProd T n x

The volume factor is at least 1. Every factor max 1 σᵢ ≥ 1, so the product is ≥ 1.

theorem Oseledets.volProd_pos {d : ℕ} (T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (n : ℕ) (x : EuclideanSpace ℝ (Fin d)) : 0 < volProd T n x

The volume factor is positive. Immediate from one_le_volProd.

theorem Oseledets.log_volProd_eq_sum_posLog {d : ℕ} (T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (n : ℕ) (x : EuclideanSpace ℝ (Fin d)) : Real.log (volProd T n x) = ∑ i ∈ Finset.range d, ((Matrix.toEuclideanLin (cocycle (derivativeCocycle T) T n x)).singularValues i).posLog

The log of the volume factor is the positive-part log-singular-value sum. log (volProd T n x) = ∑_{i<d} log⁺ σᵢ(D_x(T^[n])). This is the Oseledets.Entropy.sum_posLog_singularValues_toEuclideanLin_eq identity, read right-to-left and specialized to the cocycle iterate.

The orbit growth rate

theorem Oseledets.sum_max_zero_exponents_eq_sumPosExp {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hT : Ergodic T μ) (hdet : ∀ (x : EuclideanSpace ℝ (Fin d)), (derivativeCocycle T x).det ≠ 0) (hint : IntegrableLogNorm (derivativeCocycle T) μ) (hint' : IntegrableLogNorm (fun (x : EuclideanSpace ℝ (Fin d)) => (derivativeCocycle T x)⁻¹) μ) : ∑ i : Fin d, max 0 (exponents hT hdet ⋯ hint hint' i) = sumPosExp hT hdet ⋯ hint hint'

The positive part of the spectrum sums to the positive-exponent sum. Summing the truncated exponents max 0 (exponents i) over all indices gives the sum of the strictly positive exponents sumPosExp: a non-positive exponent contributes max 0 (exponents i) = 0, and a positive one contributes itself. This is the deterministic, ergodic-constant right-hand side of the sharp Ruelle inequality, expressed as the limit value of the orbit rate.

theorem Oseledets.tendsto_posLog_singularValue {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hT : Ergodic T μ) (hdet : ∀ (x : EuclideanSpace ℝ (Fin d)), (derivativeCocycle T x).det ≠ 0) (hint : IntegrableLogNorm (derivativeCocycle T) μ) (hint' : IntegrableLogNorm (fun (x : EuclideanSpace ℝ (Fin d)) => (derivativeCocycle T x)⁻¹) μ) (i : Fin d) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * ((Matrix.toEuclideanLin (cocycle (derivativeCocycle T) T n x)).singularValues ↑i).posLog) Filter.atTop (nhds (max 0 (exponents hT hdet ⋯ hint hint' i)))

The per-index orbit rate limit. For μ-a.e. x and each singular-value index i, the normalized positive-part log of the i-th singular value of the cocycle iterate converges to the truncated exponent max 0 (exponents i). Because (n)⁻¹ ≥ 0, the prefactor commutes with the truncation, (n)⁻¹ · log⁺ σᵢ = max 0 ((n)⁻¹ log σᵢ); continuity of max 0 · (Filter.Tendsto.max_left) applied to the per-exponent singular-value limit Oseledets.exponents_tendsto_log_singularValue gives the result.

theorem Oseledets.tendsto_log_volProd {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hT : Ergodic T μ) (hdet : ∀ (x : EuclideanSpace ℝ (Fin d)), (derivativeCocycle T x).det ≠ 0) (hint : IntegrableLogNorm (derivativeCocycle T) μ) (hint' : IntegrableLogNorm (fun (x : EuclideanSpace ℝ (Fin d)) => (derivativeCocycle T x)⁻¹) μ) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (volProd T n x)) Filter.atTop (nhds (sumPosExp hT hdet ⋯ hint hint'))

The orbit growth rate (the new orbit-iteration content). For μ-a.e. x, the normalized log of the per-orbit positive-part singular-value product converges to the sum of the strictly positive Lyapunov exponents:

(1/n) · log (volProd T n x) → sumPosExp.

This is the sharp finite-n volume rate driving the Ruelle counting bound. Rewriting log (volProd …) = ∑_{i<d} log⁺ σᵢ (log_volProd_eq_sum_posLog) and distributing the (n)⁻¹ prefactor over the finite sum, each term converges to max 0 (exponents i) (tendsto_posLog_singularValue); the finite sum of the limits is ∑ᵢ max 0 (exponents i) = sumPosExp (sum_max_zero_exponents_eq_sumPosExp). No additional Furstenberg–Kesten integrability for a compound generator is required: the rate rides entirely on the per-exponent singular-value limits.

theorem Oseledets.eventually_volProd_le {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hT : Ergodic T μ) (hdet : ∀ (x : EuclideanSpace ℝ (Fin d)), (derivativeCocycle T x).det ≠ 0) (hint : IntegrableLogNorm (derivativeCocycle T) μ) (hint' : IntegrableLogNorm (fun (x : EuclideanSpace ℝ (Fin d)) => (derivativeCocycle T x)⁻¹) μ) {x : EuclideanSpace ℝ (Fin d)} (hx : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (volProd T n x)) Filter.atTop (nhds (sumPosExp hT hdet ⋯ hint hint'))) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, volProd T n x ≤ Real.exp (↑n * (sumPosExp hT hdet ⋯ hint hint' + ε))

Eventual sub-exponential volProd bound at the orbit rate. At a point x where the orbit rate holds (tendsto_log_volProd), for every ε > 0 the per-orbit volume factor is eventually bounded by exp(n · (sumPosExp + ε)). This is the multiplicative form of the rate limit, obtained by exponentiating the eventual estimate (1/n) log (volProd …) ≤ sumPosExp + ε (valid for n ≥ 1 once (1/n) log volProd is within ε of sumPosExp) and using volProd > 0.

The orbit assembly: from a volProd atom-count bound to h(P, T) ≤ sumPosExp

theorem Oseledets.ksEntropyPartition_le_sumPosExp_of_atomVolProd {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hT : Ergodic T μ) (hdet : ∀ (x : EuclideanSpace ℝ (Fin d)), (derivativeCocycle T x).det ≠ 0) (hint : IntegrableLogNorm (derivativeCocycle T) μ) (hint' : IntegrableLogNorm (fun (x : EuclideanSpace ℝ (Fin d)) => (derivativeCocycle T x)⁻¹) μ) {ι : Type u_1} [Fintype ι] [Nonempty ι] (P : Entropy.MeasurePartition μ ι) {C : ℝ} (hC : 1 ≤ C) {x : EuclideanSpace ℝ (Fin d)} (hxrate : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (volProd T n x)) Filter.atTop (nhds (sumPosExp hT hdet ⋯ hint hint'))) (hatom : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Entropy.atomCount ⋯ P n) ≤ C * volProd T n x) : Entropy.ksEntropyPartition ⋯ P ≤ sumPosExp hT hdet ⋯ hint hint'

The orbit assembly (sorry-free). Suppose, for a finite partition P of the probability space, there is a base point x at which the orbit rate holds (hxrate, supplied a.e. by tendsto_log_volProd) and at which the non-empty atom count of the refined partition is eventually bounded by C · volProd T n x (hatom, the distilled output of the Mañé/Katok orbit covering–distortion count via the in-tree local covering count Oseledets.coveringCount_image_ball_le_volProd). Then the Kolmogorov–Sinai partition entropy is bounded by the positive-exponent sum:

h(P, T) ≤ sumPosExp.

The proof reduces h(P, T) ≤ sumPosExp + ε for every ε > 0: the orbit rate makes volProd ≤ exp(n(sumPosExp + ε)) eventually (eventually_volProd_le), so hatom gives the atom-count growth bound atomCount ≤ C · exp(n(sumPosExp + ε)), and the unconditional arithmetic reduction Oseledets.Entropy.ksEntropyPartition_le_of_atomCount_growth (Oseledets.Entropy.Ruelle.Crude) yields h(P, T) ≤ sumPosExp + ε; letting ε ↓ 0 finishes (ge_of_tendsto against the constant family, le_of_forall_pos_le_add).

theorem Oseledets.margulisRuelle_sharp_of_atomVolProd {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hT : Ergodic T μ) (hdet : ∀ (x : EuclideanSpace ℝ (Fin d)), (derivativeCocycle T x).det ≠ 0) (hint : IntegrableLogNorm (derivativeCocycle T) μ) (hint' : IntegrableLogNorm (fun (x : EuclideanSpace ℝ (Fin d)) => (derivativeCocycle T x)⁻¹) μ) (hdiff : Differentiable ℝ T) (hatom : ∀ (n : ℕ) (P : Entropy.MeasurePartition μ (Fin n)), ∃ (C : ℝ) (x : EuclideanSpace ℝ (Fin d)), 1 ≤ C ∧ Filter.Tendsto (fun (m : ℕ) => (↑m)⁻¹ * Real.log (volProd T m x)) Filter.atTop (nhds (sumPosExp hT hdet ⋯ hint hint')) ∧ ∀ᶠ (m : ℕ) in Filter.atTop, ↑(Entropy.atomCount ⋯ P m) ≤ C * volProd T m x) : Entropy.ksEntropy ⋯ ≤ ↑(sumPosExp hT hdet ⋯ hint hint')

The sharp Margulis–Ruelle inequality, conditional on the orbit atom-count input.

For an ergodic, differentiable self-map T of EuclideanSpace ℝ (Fin d) with nonsingular, log-integrable derivative cocycle, the Kolmogorov–Sinai system entropy is bounded by the sum of the strictly positive Lyapunov exponents:

h(T) ≤ ∑_{λᵢ > 0} λᵢ.

The single geometric input hatom is the honest distillation of the Mañé/Katok orbit covering–distortion count: for every finite partition P, there is a constant C ≥ 1 and a base point x at which the non-empty atom count of the n-fold refinement is eventually bounded by C · volProd T n x — the per-orbit positive-part singular-value product, whose growth rate is sumPosExp (tendsto_log_volProd). This carries the same non-compactness regime as the crude bound Oseledets.Entropy.Ruelle.Crude (a uniform-distortion hypothesis is unavoidable on the noncompact EuclideanSpace, Riquelme 2017); the surrounding orbit reduction — ksEntropyPartition_le_sumPosExp_of_atomVolProd per partition, then the supremum lift Oseledets.margulisRuelle_le_sumPosExp — is unconditional and sorry-free.

The orbit rate at the base point is not an extra hypothesis: it is supplied a.e. by tendsto_log_volProd, and a base point of the full-measure rate set carrying the atom bound is what hatom provides (its existence is the content of the geometric count, fed by the in-tree local covering count Oseledets.coveringCount_image_ball_le_volProd).