Documentation

Oseledets.Continuous.SuspensionExponentDescent

Growth-rate (Lyapunov-exponent) descent of the cover cocycle to the orbit quotient #

This module turns the two-sided bounded operator-norm bracket of Oseledets.Continuous.SuspensionGrowthDescent (the orbit re-basing coverCocycle (x, s) t = coverCocycle (suspensionAct n (x, s)) t * cocycle A T n x and its two op-norm shadows) into the limit transfer that the special-flow / suspension Lyapunov-exponent program of issue #5 needs: the growth rate lim (1/t) log ‖coverCocycle p t‖ is the same for a cover point (x, s) and its re-based orbit point suspensionAct (n : ℤ) (x, s). This is the mechanism by which the cover-cocycle growth rate — although the matrix cover cocycle does not descend to the orbit quotient SuspensionSpace T hτ — passes to the quotient: a fixed multiplicative matrix discrepancy cocycle A T n x per n orbit steps becomes a fixed additive log shift, washed out by the 1/t Birkhoff average.

This is the standard special-flow / flow-under-a-roof bookkeeping of Cornfeld–Fomin–Sinai, Ergodic Theory (Springer 1982), Ch. 11 (special/suspension flows; Ambrose–Kakutani), the first-return / ceiling construction underlying Abramov's entropy formula h(flow) = h(base)/∫τ (L. M. Abramov, On the entropy of a flow, Dokl. Akad. Nauk SSSR 128 (1959) 873–875), whose Lyapunov-exponent analogue λ_flow = λ_base / ∫τ is the headline target; the descent direction — the exponent, not the matrix, passes to the quotient — is the design reference of Bessa–Varandas (suspension Lyapunov exponents).

Main results #

gap #

The space-level statement on SuspensionSpace T hτ is assembled elsewhere (coverCocycle_tendsto_exponent_of_bddRoof for the bounded-roof section exponent, and the base-a.e.→μ̂-a.e. disintegration ae_suspensionMeasure_* of Oseledets.Continuous.SuspensionDisintegration); this file supplies only the representative-free re-basing invariance of the growth rate. The strict-positivity hypotheses on the two cover-cocycle norms are taken explicitly rather than derived here: positivity of ‖coverCocycle p t‖ holds when the base matrices A are invertible (every flowCocycleSection is then a product of invertible A-factors, hence nonzero with positive operator norm), but that derivation lives with the flowCocycleSection invertibility infrastructure and is not re-proved here. No λ_flow = λ_base / ∫τ quotient identity is claimed in this module.

source
theorem Oseledets.norm_pos_of_isUnit_det {d : ℕ} [NeZero d] {M : Matrix (Fin d) (Fin d) ℝ} (hM : IsUnit M.det) :
0 < ‖M‖

Positivity of the operator norm of an invertible matrix. If M.det is a unit then M is nonzero (the zero matrix has determinant 0 over a nonempty index type, which is not a unit), so its L2 operator norm is strictly positive. Stated in the [NeZero d] form: NeZero d provides the Nonempty (Fin d) needed for Matrix.det_zero.

source
theorem Oseledets.coverCocycle_suspensionAct_log_discrepancy {X : Type u_1} [MeasurableSpace X] {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} [NeZero d] (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (n : ℕ) (x : X) (s t : ℝ) (hst : returnTime T hτ n x ≤ s + t) (hU : IsUnit (cocycle A (⇑T) n x).det) (hp : 0 < ‖coverCocycle A T hτ hc hcpos (x, s) t‖) (hq : 0 < ‖coverCocycle A T hτ hc hcpos (suspensionAct T hτ ↑n (x, s)) t‖) :
|Real.log ‖coverCocycle A T hτ hc hcpos (suspensionAct T hτ ↑n (x, s)) t‖ - Real.log ‖coverCocycle A T hτ hc hcpos (x, s) t‖| ≤ |Real.log ‖cocycle A (⇑T) n x‖| + |Real.log ‖(cocycle A (⇑T) n x)⁻¹‖|

The t-independent additive log-discrepancy bound. Taking Real.log of the two op-norm brackets coverCocycle_suspensionAct_opNorm_le and coverCocycle_suspensionAct_opNorm_ge (valid once returnTime n x ≤ s + t), under invertibility of the base cocycle and strict positivity of both cover-cocycle norms, the two log-norms differ by at most the constant (in t) log ‖cocycle A T n x‖ + log ‖(cocycle A T n x)⁻¹‖: |log ‖coverCocycle (suspensionAct n (x, s)) t‖ − log ‖coverCocycle (x, s) t‖| ≤ log ‖cocycle A T n x‖ + log ‖(cocycle A T n x)⁻¹‖. This is the bounded multiplicative discrepancy of SuspensionGrowthDescent turned additive — the shift the 1/t Birkhoff average will wash out.

source
theorem Oseledets.coverCocycle_suspensionAct_tendsto_exponent {X : Type u_1} [MeasurableSpace X] {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} [NeZero d] (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (n : ℕ) (x : X) (s : ℝ) (hU : IsUnit (cocycle A (⇑T) n x).det) (hret : ∀ᶠ (t : ℝ) in Filter.atTop, returnTime T hτ n x ≤ s + t) (hp : ∀ᶠ (t : ℝ) in Filter.atTop, 0 < ‖coverCocycle A T hτ hc hcpos (x, s) t‖) (hq : ∀ᶠ (t : ℝ) in Filter.atTop, 0 < ‖coverCocycle A T hτ hc hcpos (suspensionAct T hτ ↑n (x, s)) t‖) {L : ℝ} (hL : Filter.Tendsto (fun (t : ℝ) => Real.log ‖coverCocycle A T hτ hc hcpos (x, s) t‖ / t) Filter.atTop (nhds L)) :
Filter.Tendsto (fun (t : ℝ) => Real.log ‖coverCocycle A T hτ hc hcpos (suspensionAct T hτ ↑n (x, s)) t‖ / t) Filter.atTop (nhds L)

The Lyapunov-exponent limit transfer (headline). If the cover-cocycle growth rate (1/t) log ‖coverCocycle (x, s) t‖ converges to L as t → ∞, the base cocycle cocycle A T n x is invertible, and both cover-cocycle norms are eventually strictly positive (for all large t), then the cover-cocycle growth rate at the re-based orbit point suspensionAct (n : ℤ) (x, s) converges to the same L: Tendsto (fun t ↦ log ‖coverCocycle (x, s) t‖ / t) atTop (𝓝 L) → Tendsto (fun t ↦ log ‖coverCocycle (suspensionAct (n : ℤ) (x, s)) t‖ / t) atTop (𝓝 L).

The per-t average at the re-based point lies within (C)/t of the average at (x, s), where C = |log ‖cocycle A T n x‖| + |log ‖(cocycle A T n x)⁻¹‖| is the t-independent additive log-discrepancy of coverCocycle_suspensionAct_log_discrepancy; since C / t → 0, a Filter.Tendsto squeeze transfers the limit. This is the representative-free invariance of the growth rate under the orbit action — the mechanism of the special-flow exponent descent.