The representative-free flow Lyapunov exponent on the suspension quotient

This module defines the flow Lyapunov exponent as a genuine property of a point of the orbit quotient SuspensionSpace T hτ (the mapping torus of T under the roof τ), and proves it is well defined: the growth rate lim (1/t) log ‖coverCocycle p t‖ of the cover cocycle does not depend on which representative (x, s) of the orbit class [x, s] is used to compute it.

The cover cocycle of Oseledets.Continuous.SuspensionCoverFlow is the cover-level special-flow cocycle: the accumulated matrix coverCocycle (x, s) t lives on X × ℝ, before passing to the quotient. As recorded in Oseledets.Continuous.SuspensionGrowthDescent, the matrix cover cocycle does not descend to the quotient — re-basing along one orbit step post-multiplies it by the fixed factor cocycle A T n x. What does descend is the growth rate: the fixed multiplicative factor becomes a fixed additive log shift, washed out by the 1/t Birkhoff average. The limit-transfer mechanism is coverCocycle_suspensionAct_tendsto_exponent (Module 1, Oseledets.Continuous.SuspensionExponentDescent); this module packages it into a representative-free predicate on SuspensionSpace.

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 descent direction — the exponent, not the matrix, passes to the quotient — is the design reference of Bessa–Varandas (suspension Lyapunov exponents). The headline analogue is 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).

Main definitions

• Oseledets.HasFlowExponent: the predicate HasFlowExponent q L on q : SuspensionSpace T hτ, asserting that some representative (x, s) of the orbit class q carries the cover-cocycle growth rate L, i.e. suspensionMk (x, s) = q and Tendsto (fun t ↦ log ‖coverCocycle (x, s) t‖ / t) atTop (𝓝 L). The existential form lifts cleanly to the quotient; the well-definedness theorems below show the growth rate is in fact the same for every representative under invertibility.

Main results

• Oseledets.tendsto_exponent_iff_of_suspensionAct: the two-sided well-definedness for a forward orbit step. If suspensionAct (n : ℤ) (x, s) = (x₂, s₂) for a natural n, and the base cocycle is invertible with both cover-cocycle norms eventually strictly positive, then the cover-cocycle growth rates at (x, s) and at (x₂, s₂) converge to L for the same L: the two Tendsto statements are equivalent. The → direction is the Module-1 limit transfer; the ← direction is its mirror, obtained from the symmetric additive log-discrepancy bound coverCocycle_suspensionAct_log_discrepancy by the same 1/t squeeze.
• Oseledets.hasFlowExponent_of_suspensionAct: orbit-class invariance of HasFlowExponent. If two cover points are connected by a forward orbit step suspensionAct (n : ℤ) (x, s) = (x₂, s₂) (so suspensionMk (x, s) = suspensionMk (x₂, s₂)) then, under the same hypotheses, Tendsto (fun t ↦ log ‖coverCocycle (x, s) t‖ / t) atTop (𝓝 L) witnesses HasFlowExponent (suspensionMk (x₂, s₂)) L: the growth rate computed at one representative certifies the exponent of the whole orbit class.

gap

The two well-definedness results are keyed on a forward orbit step suspensionAct (n : ℤ) with n : ℕ. Orbit equivalence in SuspensionSpace — suspensionMk (x, s) = suspensionMk (x₂, s₂) — unfolds (via Quotient.eq and AddAction.mem_orbit_iff) to a signed integer m : ℤ with suspensionAct m (x₂, s₂) = (x, s). Closing the well-definedness over the full signed-integer connection (the m < 0 case, i.e. a backward orbit step) requires re-running the Module-1 re-basing in the inverse direction; the orbit re-basing identity coverCocycle_suspensionAct_rebasing is stated for n : ℕ, so the negative branch would apply it with the roles of the two points swapped. That signed-integer closure — and hence the fully representative-free Quotient.lift of the exponent to a function SuspensionSpace → ℝ and its μ̂-a.e. identification with λ_base / ∫τ — is deferred. This module supplies the forward-step well-definedness, which is the orbit-invariance content (the orbit of any point is generated by the single forward step and its inverse). No λ_flow = λ_base / ∫τ quotient identity is claimed here.

def Oseledets.HasFlowExponent {X : Type u_1} [MeasurableSpace X] {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (q : SuspensionSpace T hτ) (L : ℝ) : Prop

The flow Lyapunov exponent of a point of the suspension quotient. HasFlowExponent q L holds when some representative (x, s) of the orbit class q : SuspensionSpace T hτ carries the cover-cocycle growth rate L: suspensionMk (x, s) = q ∧ Tendsto (fun t ↦ log ‖coverCocycle (x, s) t‖ / t) atTop (𝓝 L).

The existential form is what lifts cleanly to the quotient (a property of some representative); the well-definedness theorems tendsto_exponent_iff_of_suspensionAct / hasFlowExponent_of_suspensionAct show that, under base-cocycle invertibility, the growth rate is the same for every representative — so HasFlowExponent q L is a genuine property of the orbit class q.

Equations

• One or more equations did not get rendered due to their size.

theorem Oseledets.tendsto_exponent_iff_of_suspensionAct {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 : ℝ} : 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)

Two-sided well-definedness across a forward orbit step. If the cover point (x₂, s₂) is the forward orbit image suspensionAct (n : ℤ) (x, s) for a natural n, the base cocycle is invertible, and both cover-cocycle norms are eventually strictly positive, then the cover-cocycle growth rates at (x, s) and at (x₂, s₂) converge to one and the same L: Tendsto (fun t ↦ log ‖coverCocycle (x, s) t‖ / t) atTop (𝓝 L) ↔ Tendsto (fun t ↦ log ‖coverCocycle (x₂, s₂) t‖ / t) atTop (𝓝 L).

The → direction is the Module-1 limit transfer coverCocycle_suspensionAct_tendsto_exponent. The ← direction is its mirror: the additive log-discrepancy bound coverCocycle_suspensionAct_log_discrepancy is symmetric in the two points, so the per-t average at (x, s) lies within C / t of the average at the re-based point, and the same Filter.Tendsto squeeze transfers the limit the other way.

theorem Oseledets.hasFlowExponent_of_suspensionAct {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 : ℝ) {x₂ : X} {s₂ : ℝ} (hxs : suspensionAct T hτ ↑n (x, s) = (x₂, s₂)) {L : ℝ} (hL : Filter.Tendsto (fun (t : ℝ) => Real.log ‖coverCocycle A T hτ hc hcpos (x, s) t‖ / t) Filter.atTop (nhds L)) : HasFlowExponent A T hτ hc hcpos (suspensionMk T hτ (x₂, s₂)) L

Orbit-class invariance of the flow exponent. If two cover points are connected by a forward orbit step suspensionAct (n : ℤ) (x, s) = (x₂, s₂) (so suspensionMk (x, s) = suspensionMk (x₂, s₂)), then — under base-cocycle invertibility and eventual strict positivity of both cover-cocycle norms — the growth rate L computed at the representative (x, s) certifies the flow exponent of the orbit class of (x₂, s₂): it produces a HasFlowExponent (suspensionMk (x₂, s₂)) L witness. This is the well-definedness of the flow exponent under (forward) orbit equivalence: the exponent is a property of the class, read off from any representative.

The orbit step hxs is used to identify the two orbit classes (suspensionMk of orbit-equivalent points agree); the growth rate at (x, s) then directly witnesses the exponent of the common class. (No invertibility is needed for this direction — (x, s) itself serves as the witness; invertibility enters only in tendsto_exponent_iff_of_suspensionAct, which guarantees the same L is obtained from the other representative (x₂, s₂).)