Documentation

Oseledets.Continuous.SuspensionBddRoofExponent

The full-time special-flow exponent under a bounded roof #

This module closes the section-level full-time special-flow Lyapunov exponent λ_flow = λ_base / ∫τ (the headline of Issue #5) under the natural extra hypothesis that the roof τ is bounded above, τ ≤ C. The reduction lemmas Oseledets.coverCocycle_norm_eq_lapCount and Oseledets.log_coverCocycle_div_eq_lapCount (of Oseledets.Continuous.SuspensionFullTimeExponent) already factor the full-time Birkhoff ratio exactly as

log‖coverCocycle (x,0) t‖ / t = (returnTime (lapCount t x) x / t) · (log‖cocycle A T (lapCount t x) x‖ / returnTime (lapCount t x) x),

a product of a time-distortion factor and a return-time exponent ratio. The SuspensionFullTimeExponent header records the precise remaining analytic gap: with only a uniform lower bound c ≤ τ, the time-distortion factor returnTime (lapCount t x) x / t cannot be squeezed to 1 (the lap width returnTime (n+1) x − returnTime n x = τ (Tⁿ x) is unbounded). The present file supplies exactly the missing analytic input: with a uniform upper bound τ ≤ C the lap width is bounded by C, the first-passage sandwich tightens to

returnTime (lapCount t x) x ≤ t < returnTime (lapCount t x) x + C,

and the time-distortion factor is squeezed to 1.

This is the special-flow / flow-under-a-roof construction 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); the Lyapunov-exponent analogue is the design reference of Bessa–Varandas (suspension Lyapunov exponents).

Main results #

What is not in this file — the precise remaining gap #

The convergence below is the section-level (cover) full-time exponent on the base cross-section: coverCocycle (x, 0) · is the suspension flow cocycle read from height 0. Two pieces remain toward the genuine space-level headline against the invariant suspension measure:

  1. Quotient descent to SuspensionSpace. Reading the rate as a class-invariant measurable function on the orbit quotient Oseledets.SuspensionSpace T hτ (the (x, τ x) ∼ (T x, 0) identification) is the open keystone, the genuine space-level FlowCocycle (cf. the quotient gap documented in Oseledets.Continuous.SuspensionCocycle).
  2. MeasurePreservingFlow packaging. Reading λ_flow = λ_base / ∫τ against the invariant suspension measure μ̂ needs per-time measure-preservation of the suspension flow. The denominator ∫τ is Abramov's; the numerator is the base Oseledets exponent.

Under the bounded-roof hypothesis the full real-time section exponent is now sorry-free; only the quotient descent and the measure-preservation packaging remain.

source
theorem Oseledets.returnTime_succ_eq {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℕ) (x : X) :
returnTime T hτ (n + 1) x = returnTime T hτ n x + τ (baseIter T hτ (↑n) x)

The return-time step. Advancing one lap adds the roof value at the shifted base point: returnTime (n + 1) x = returnTime n x + τ (baseIter T hτ n x). This unfolds the return time as the roof Birkhoff sum and applies the roof-cocycle step roofSum_add_one.

source
theorem Oseledets.returnTime_succ_le_add_C {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {C : ℝ} (hC : ∀ (x : X), τ x ≤ C) (n : ℕ) (x : X) :
returnTime T hτ (n + 1) x ≤ returnTime T hτ n x + C

Bounded lap width. Under a roof bounded above by C (τ ≤ C), one lap takes at most flow time C: returnTime (n + 1) x ≤ returnTime n x + C. Combined with the lower bound c ≤ τ this pins each lap width into [c, C].

source
theorem Oseledets.lapCount_returnTime_lt_add_C {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c C : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (hC : ∀ (x : X), τ x ≤ C) {t : ℝ} (ht : 0 ≤ t) (x : X) :
t < returnTime T hτ (lapCount T hτ hc hcpos t x) x + C

The tightened upper sandwich. Under τ ≤ C the next return overshoots t by at most C: t < returnTime (lapCount t x) x + C. This is the upper first-passage bound t < returnTime (lapCount t x + 1) x (lapCount_lt_returnTime_succ) combined with the bounded lap width returnTime (lapCount t x + 1) x ≤ returnTime (lapCount t x) x + C. Together with the lower bound returnTime (lapCount t x) x ≤ t (lapCount_returnTime_le) it confines t to a window of width C above the lap's return time — the input that squeezes the time-distortion factor.

source
theorem Oseledets.le_lapCount_of_returnTime_le {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) {n : ℕ} {t : ℝ} (x : X) (hnt : returnTime T hτ n x ≤ t) :
n ≤ lapCount T hτ hc hcpos t x

The lap count is at least n once t has reached the n-th return. For returnTime n x ≤ t the flow has completed at least n laps: n ≤ lapCount t x. This is read off from the upper first-passage bound t < returnTime (lapCount t x + 1) x through strict monotonicity of the return times. It is the engine of lapCount_tendsto_atTop.

source
theorem Oseledets.lapCount_tendsto_atTop {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (x : X) :
Filter.Tendsto (fun (t : ℝ) => lapCount T hτ hc hcpos t x) Filter.atTop Filter.atTop

The lap count diverges. As the real flow time t → ∞ the number of completed laps tends to +∞: lapCount t x → ∞. For each target n the return time returnTime n x is a witness: once t ≥ returnTime n x the flow has completed at least n laps (le_lapCount_of_returnTime_le).

source
theorem Oseledets.lapCount_returnTime_div_tendsto_one {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c C : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (hC : ∀ (x : X), τ x ≤ C) (x : X) :
Filter.Tendsto (fun (t : ℝ) => returnTime T hτ (lapCount T hτ hc hcpos t x) x / t) Filter.atTop (nhds 1)

The time-distortion factor tends to 1. Under the bounded roof τ ≤ C, the ratio of the lap's return time to the elapsed flow time converges to 1: returnTime (lapCount t x) x / t → 1 as the real t → ∞. This is the missing analytic input of the between-returns squeeze. The tightened sandwich returnTime (lapCount t x) x ≤ t < returnTime (lapCount t x) x + C confines the factor to 1 − C/t < returnTime (lapCount t x) x / t ≤ 1, and 1 − C/t → 1, so the squeeze closes.

source
theorem Oseledets.coverCocycle_tendsto_exponent_of_bddRoof {X : Type u_1} [MeasurableSpace X] {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c C : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (hC : ∀ (x : X), τ x ≤ C) {μ : MeasureTheory.Measure X} {lam : ℝ} (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τne : ∫ (y : X), τ y ∂μ ≠ 0) :
∀ᵐ (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 ∂μ))

The full-time section special-flow exponent under a bounded roof (headline). Suppose the base cocycle A has a μ-a.e. log-norm growth rate lam (n⁻¹·log‖cocycle A T n x‖ → lam a.e.; the discrete Oseledets/Furstenberg–Kesten output, taken as a hypothesis so the lemma applies to the top exponent or any other rate), the roof average converges a.e. to ∫τ, ∫τ ≠ 0, and the roof is bounded c ≤ τ ≤ C. Then the cover flow cocycle log-norm, read from the base section and rescaled by the real elapsed flow time t, converges μ-a.e. to lam / ∫τ as t → ∞: Real.log ‖coverCocycle (x, 0) t‖ / t → lam / ∫τ.

This is the full real-time upgrade of coverCocycle_returnTime_tendsto_exponent (which holds only along the discrete return subsequence). The proof runs the between-returns squeeze: by log_coverCocycle_div_eq_lapCount the ratio factors as the time-distortion factor times the return-time exponent ratio. The time-distortion factor tends to 1 via lapCount_returnTime_div_tendsto_one (the bounded-roof input). The exponent ratio is the discrete return-time exponent sampled at the lap count, tending to lam / ∫τ by composing coverCocycle_returnTime_tendsto_exponent with lapCount_tendsto_atTop and the norm bridge coverCocycle_returnTime_norm_eq. The product of the two limits is (lam / ∫τ)·1 = lam / ∫τ.