Expanding maps and the Rokhlin/Pesin right-hand-side identity

For a differentiable self-map T : E → E of E := EuclideanSpace ℝ (Fin d) we call T uniformly expanding when there is an expansion constant K > 1 with K · ‖v‖ ≤ ‖Dₓ T v‖ for every base point x and every tangent vector v. By the chain rule this expansion compounds along the orbit: the derivative of the n-th iterate satisfies Kⁿ · ‖v‖ ≤ ‖D(T^[n]) v‖. Consequently every singular value of the cocycle iterate is at least Kⁿ, so every Lyapunov exponent of the tangent cocycle is at least log K > 0.

When all Lyapunov exponents are positive the positive-part filter is everything, so the sum of the strictly positive exponents ∑λ⁺ (the Pesin / Margulis–Ruelle right-hand side, the entropy of an SRB measure) coincides with the sum of all exponents, which by the trace–determinant identity equals ∫ log|det Dₓ T| dμ (the Rokhlin right-hand side, the integrated volume distortion). This is the honest, foliation-free version of the Ledrappier–Young/Rokhlin entropy formula in the expanding case: no stable foliation, no SRB-density machinery — just the all-positive-spectrum collapse of the positive-part sum onto the determinant integral.

Main definitions

• Oseledets.IsExpanding — uniform derivative expansion ∃ K > 1, ∀ x v, K‖v‖ ≤ ‖Dₓ T v‖.

Main results

• Oseledets.cocycle_expanding_bound — the compounded bound Kⁿ‖v‖ ≤ ‖D(T^[n]) v‖.
• Oseledets.expanding_pow_le_singularValues — Kⁿ ≤ σᵢ(A⁽ⁿ⁾) for every i < d.
• Oseledets.log_le_exponents_of_expanding — every Lyapunov exponent is ≥ log K.
• Oseledets.exponents_pos_of_expanding — every Lyapunov exponent is strictly positive.
• Oseledets.sumPosExp_eq_sumAllExp_of_expanding — for an expanding map ∑λ⁺ = ∑λ.
• Oseledets.sumPosExp_eq_integral_log_abs_det_of_expanding — the Pesin = Rokhlin identity ∑λ⁺ = ∫ log|det Dₓ T| dμ.

References

• D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58.
• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

def Oseledets.IsExpanding {d : ℕ} (T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) : Prop

A differentiable self-map T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d) is uniformly expanding when there is an expansion constant K > 1 such that the derivative Dₓ T stretches every tangent vector by at least K: K · ‖v‖ ≤ ‖Dₓ T v‖ for every base point x and every vector v.

Equations

• Oseledets.IsExpanding T = ∃ (K : ℝ), 1 < K ∧ ∀ (x v : EuclideanSpace ℝ (Fin d)), K * ‖v‖ ≤ ‖(fderiv ℝ T x) v‖

theorem Oseledets.cocycle_expanding_bound {d : ℕ} {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hdiff : Differentiable ℝ T) {K : ℝ} (hK : 1 < K) (hexp : ∀ (x v : EuclideanSpace ℝ (Fin d)), K * ‖v‖ ≤ ‖(fderiv ℝ T x) v‖) (n : ℕ) (x v : EuclideanSpace ℝ (Fin d)) : K ^ n * ‖v‖ ≤ ‖(fderiv ℝ T^[n] x) v‖

The compounded expansion bound. For a differentiable uniformly expanding map with expansion constant K, the derivative of the n-th iterate stretches every vector by at least Kⁿ: Kⁿ · ‖v‖ ≤ ‖D(T^[n]) v‖. Proved by induction on n, using the chain rule D(T^[n+1]) x = D(T^[n]) (T x) ∘ Dₓ T to peel off one expanding factor at each step.

theorem Oseledets.cocycle_expanding_bound_clm {d : ℕ} {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hdiff : Differentiable ℝ T) {K : ℝ} (hK : 1 < K) (hexp : ∀ (x v : EuclideanSpace ℝ (Fin d)), K * ‖v‖ ≤ ‖(fderiv ℝ T x) v‖) (n : ℕ) (x v : EuclideanSpace ℝ (Fin d)) : K ^ n * ‖v‖ ≤ ‖(Matrix.toEuclideanCLM (cocycle (derivativeCocycle T) T n x)) v‖

Compounded expansion in cocycle form. The matrix cocycle iterate toEuclideanCLM (cocycle (derivativeCocycle T) T n x) stretches every vector by at least Kⁿ. This is cocycle_expanding_bound transported through the chain-rule cocycle identity chainRule_cocycle.

A uniform lower bound on the norm implies a lower bound on all singular values

theorem Oseledets.le_singularValues_of_forall_le {d : ℕ} {f : EuclideanSpace ℝ (Fin d) →ₗ[ℝ] EuclideanSpace ℝ (Fin d)} {c : ℝ} (hf : ∀ (v : EuclideanSpace ℝ (Fin d)), c * ‖v‖ ≤ ‖f v‖) {i : ℕ} (hi : i < d) : c ≤ f.singularValues i

A uniform lower bound on the stretching of a linear endomorphism of EuclideanSpace ℝ (Fin d) forces every one of its d singular values to be at least that bound: if c · ‖v‖ ≤ ‖f v‖ for every v, then c ≤ σᵢ(f) for each i < d. The proof evaluates f on the (unit-norm) right singular vector uᵢ, where σᵢ(f) = ‖f uᵢ‖ ≥ c · ‖uᵢ‖ = c.

theorem Oseledets.expanding_pow_le_singularValues {d : ℕ} {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hdiff : Differentiable ℝ T) {K : ℝ} (hK : 1 < K) (hexp : ∀ (x v : EuclideanSpace ℝ (Fin d)), K * ‖v‖ ≤ ‖(fderiv ℝ T x) v‖) (n : ℕ) (x : EuclideanSpace ℝ (Fin d)) {i : ℕ} (hi : i < d) : K ^ n ≤ (Matrix.toEuclideanLin (cocycle (derivativeCocycle T) T n x)).singularValues i

Every singular value is at least Kⁿ. For a differentiable uniformly expanding map with constant K, every singular value of the cocycle iterate A⁽ⁿ⁾ = cocycle (derivativeCocycle T) T n is at least Kⁿ (for i < d). Combines cocycle_expanding_bound_clm (the uniform stretching bound) with le_singularValues_of_forall_le, identifying toEuclideanCLM with toEuclideanLin.

Every Lyapunov exponent is at least log K, hence positive

theorem Oseledets.log_le_exponents_of_expanding {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) {K : ℝ} (hK : 1 < K) (hexp : ∀ (x v : EuclideanSpace ℝ (Fin d)), K * ‖v‖ ≤ ‖(fderiv ℝ T x) v‖) (i : Fin d) : Real.log K ≤ exponents hT hdet ⋯ hint hint' i

Every Lyapunov exponent is at least log K. For an ergodic, log-integrable, differentiable uniformly expanding map with constant K, each Lyapunov exponent of the tangent cocycle is at least log K. The per-index σ-limit (1/n) log σᵢ(A⁽ⁿ⁾) → exponents i holds μ-a.e. (exponents_tendsto_log_singularValue); by expanding_pow_le_singularValues the pre-limit terms are ≥ (1/n) log Kⁿ = log K, so the limit inherits the bound.

theorem Oseledets.exponents_pos_of_expanding {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) {K : ℝ} (hK : 1 < K) (hexp : ∀ (x v : EuclideanSpace ℝ (Fin d)), K * ‖v‖ ≤ ‖(fderiv ℝ T x) v‖) (i : Fin d) : 0 < exponents hT hdet ⋯ hint hint' i

Every Lyapunov exponent of an expanding map is strictly positive. Since each exponent is at least log K and K > 1 gives log K > 0, every exponent is positive.

theorem Oseledets.sumPosExp_eq_sumAllExp_of_expanding {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) {K : ℝ} (hK : 1 < K) (hexp : ∀ (x v : EuclideanSpace ℝ (Fin d)), K * ‖v‖ ≤ ‖(fderiv ℝ T x) v‖) : sumPosExp hT hdet ⋯ hint hint' = sumAllExp hT hdet ⋯ hint hint'

For an expanding map, the positive-exponent sum is the full exponent sum. Because every Lyapunov exponent is strictly positive, the positive-part filter {i | 0 < exponents i} is all of Finset.univ, so ∑λ⁺ = ∑λ.

theorem Oseledets.sumPosExp_eq_integral_log_abs_det_of_expanding {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) {K : ℝ} (hK : 1 < K) (hexp : ∀ (x v : EuclideanSpace ℝ (Fin d)), K * ‖v‖ ≤ ‖(fderiv ℝ T x) v‖) : sumPosExp hT hdet ⋯ hint hint' = ∫ (x : EuclideanSpace ℝ (Fin d)), Real.log |(derivativeCocycle T x).det| ∂μ

The Pesin = Rokhlin right-hand-side identity for an expanding map. For an ergodic, log-integrable, differentiable uniformly expanding self-map T, the sum of the strictly positive Lyapunov exponents — the Pesin / Margulis–Ruelle right-hand side ∑λ⁺ — equals the integral of log|det Dₓ T| — the Rokhlin right-hand side (integrated volume distortion): ∑λ⁺ = ∫ log|det Dₓ T| dμ.

This is the honest, foliation-free instance of the entropy formula: since all exponents are positive, ∑λ⁺ = ∑λ (sumPosExp_eq_sumAllExp_of_expanding), and the trace–determinant identity sumAllExp_eq_integral_log_abs_det rewrites ∑λ as ∫ log|det A|.