The space-level special-flow Lyapunov exponent value λ_base / ∫τ

This module assembles the space-level headline of Issue #5: for the suspension (mapping-torus) space SuspensionSpace T hτ of the base map T under the roof τ, the flow Lyapunov exponent HasFlowExponent q (λ_base / ∫τ) holds for μ̂-almost every orbit class q, where μ̂ is the invariant probability measure suspensionMeasure and λ_base is the top base Lyapunov exponent. This is the Lyapunov-exponent analogue of 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), in the special-flow / flow-under-a-roof setting of Cornfeld–Fomin–Sinai, Ergodic Theory (Springer 1982), Ch. 11 (special/suspension flows; Ambrose–Kakutani); the exponent-transfer direction is the design reference of Bessa–Varandas (suspension Lyapunov exponents).

The assembly combines three already-built pieces:

• the bounded-roof cross-section exponent coverCocycle_tendsto_exponent_of_bddRoof (Oseledets.Continuous.SuspensionBddRoofExponent), giving for base-μ-a.e. x the section growth rate Real.log ‖coverCocycle (x, 0) t‖ / t → λ_base / ∫τ (read off the base section, height s = 0);
• the disintegration / fundamental-domain transfer ae_suspensionMeasure_section_exponent_set (Oseledets.Continuous.SuspensionDisintegration), lifting that base-a.e. set of section exponents to a μ̂-a.e. set of orbit classes admitting a box representative (x, s) whose first coordinate carries the section exponent;
• the HasFlowExponent predicate (Oseledets.Continuous.SuspensionSpaceExponent), the representative-free flow exponent on SuspensionSpace.

The one new ingredient is the height-shift step tendsto_coverCocycle_exponent_of_section: the section growth rate at the base point (x, 0) equals the cover-cocycle growth rate at every height (x, s). This is immediate from coverCocycle (x, s) t = coverCocycle (x, 0) (s + t) (unfolding Oseledets.coverCocycle = flowCocycleSection (p.2 + t) p.1): the per-t ratio log ‖coverCocycle (x, s) t‖ / t is the section ratio at total time s + t rescaled by (s + t) / t → 1, so the two limits coincide. The base representative (x, s) — the actual representative q = [x, s] the disintegration hands back — is then a HasFlowExponent witness for its own class.

Main results

• Oseledets.tendsto_coverCocycle_exponent_of_section: the height-shift. If Real.log ‖coverCocycle (x, 0) t‖ / t → L, then Real.log ‖coverCocycle (x, s) t‖ / t → L for every height s.
• Oseledets.ae_suspensionMeasure_hasFlowExponent: the space-level exponent. Under a bounded roof c ≤ τ ≤ C with 0 < c, positive integral 0 < ∫τ, and the base-a.e. Birkhoff growth / roof-average limits (top base exponent λ_base, mean roof ∫τ), for μ̂-a.e. q ∈ SuspensionSpace, HasFlowExponent q (λ_base / ∫τ).

gap

The headline is the μ̂-a.e. existence of the flow exponent value λ_base / ∫τ at almost every class — the genuine space-level #5 exponent. It is the μ̂-a.e. instantiation of the existential predicate HasFlowExponent; uniqueness of that value across the class (well-definedness of a single SuspensionSpace → ℝ exponent function) is the forward-step content of Oseledets.tendsto_exponent_iff_of_suspensionAct (SuspensionSpaceExponent), whose closure over the full signed-integer orbit connection is deferred there. The measurability witness hmeas of the lifted exponent set on the quotient is consumed as an explicit hypothesis (the disintegration data, exactly as in ae_suspensionMeasure_section_exponent_set: the quotient image of a measurable base set is not measurable for free). No closed-form identification of λ_base with the integrated top Lyapunov exponent is asserted here beyond its defining base-a.e. Birkhoff limit hgrow.

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

Height-shift of the cover-cocycle exponent. The section growth rate read at the base point (x, 0) propagates to every height (x, s): if Real.log ‖coverCocycle (x, 0) t‖ / t → L, then Real.log ‖coverCocycle (x, s) t‖ / t → L.

Since coverCocycle (x, s) t = flowCocycleSection (s + t) x = coverCocycle (x, 0) (s + t), the height-s ratio at flow time t equals the section ratio at total time s + t times the rescaling (s + t) / t. As t → ∞ the section ratio tends to L (composition with t ↦ s + t → atTop) and (s + t) / t = 1 + s / t → 1, so the product tends to L.

theorem Oseledets.ae_suspensionMeasure_hasFlowExponent {X : Type u_1} [MeasurableSpace X] {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c C : ℝ} {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] {lam : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (hC : ∀ (x : X), τ x ≤ C) (hPmeas : MeasurableSet {x : X | Filter.Tendsto (fun (t : ℝ) => Real.log ‖coverCocycle A T hτ hc hcpos (x, 0) t‖ / t) Filter.atTop (nhds (lam / ∫ (y : X), τ y ∂μ))}) (hmeas : MeasurableSet {q : SuspensionSpace T hτ | ∃ (p : X × ℝ), suspensionMk T hτ p = q ∧ Filter.Tendsto (fun (t : ℝ) => Real.log ‖coverCocycle A T hτ hc hcpos (p.1, 0) t‖ / t) Filter.atTop (nhds (lam / ∫ (y : X), τ y ∂μ))}) (hgrow : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖cocycle A (⇑T) n x‖) Filter.atTop (nhds lam)) (hroof : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * roofSum T hτ (↑n) x) Filter.atTop (nhds (∫ (y : X), τ y ∂μ))) (hτ_pos : 0 < ∫ (y : X), τ y ∂μ) : ∀ᵐ (q : SuspensionSpace T hτ) ∂suspensionMeasure T hτ μ, HasFlowExponent A T hτ hc hcpos q (lam / ∫ (y : X), τ y ∂μ)

The space-level special-flow Lyapunov exponent. For the suspension space SuspensionSpace T hτ with its invariant probability measure μ̂ = suspensionMeasure, under a bounded roof c ≤ τ ≤ C (0 < c), positive integral 0 < ∫τ, and the base-a.e. Birkhoff limits — the discrete base growth rate → λ_base and the roof average → ∫τ — the flow Lyapunov exponent equals λ_base / ∫τ for μ̂-almost every orbit class: ∀ᵐ q ∂μ̂, HasFlowExponent q (λ_base / ∫τ).

The base-a.e. section exponent coverCocycle_tendsto_exponent_of_bddRoof is transferred to a μ̂-a.e. set of classes by the disintegration ae_suspensionMeasure_section_exponent_set, handing back, for μ̂-a.e. q, a box representative (x, s) with suspensionMk (x, s) = q and the section exponent at (x, 0). The height-shift tendsto_coverCocycle_exponent_of_section promotes that section exponent to the cover-cocycle exponent at the actual representative (x, s), which then witnesses HasFlowExponent q (λ_base / ∫τ).

hmeas (measurability of the lifted exponent set on the quotient) is the disintegration datum required by ae_suspensionMeasure_section_exponent_set — the quotient image of a measurable base set is not measurable for free — and is carried through as an explicit hypothesis.