The return-time exponent of a suspension

This module isolates the mathematical core of the suspension exponent-transfer identity

λ_flow = λ_base / ∫ τ,

namely the denominator ∫ τ and the rescaling of the base index n by the roof Birkhoff sum roofSum n (the return time after n base steps). The full flow-cocycle and its identification with the base cocycle along the cross-section are deferred to a follow-up module; here we land the base-only statement, which already captures the limit n / roofSum n x → 1 / ∫ τ and combines it with an arbitrary base exponent to produce the rescaled exponent λ_base / ∫ τ.

Main results

• Oseledets.tendsto_div_of_tendsto_div: a pure real-analysis ratio lemma — if n⁻¹ · a n → L and n⁻¹ · r n → R ≠ 0 then a n / r n → L / R.
• Oseledets.roofSum_natCast_eq_birkhoffSum: the reconciliation of the integer-indexed roofSum (restricted to ℕ) with Mathlib's Function.birkhoffSum of the roof along the base map; the crux that turns the suspension roof cocycle into a Birkhoff sum.
• Oseledets.tendsto_roofAverage_ae: under ergodicity and integrability of τ, the roof average n⁻¹ · roofSum n x converges μ-a.e. to ∫ τ (the ergodic Birkhoff theorem applied to the roof).
• Oseledets.integral_roof_pos: positivity of ∫ τ from a uniform lower bound on τ and a probability measure.
• Oseledets.returnTime_tendsto_exponent: the return-time exponent. Given any base log-norm growth rate lam (a hypothesis, so the lemma applies to the top exponent, a k-th exponent, etc.), the cocycle log-norm rescaled by the return time roofSum n x converges μ-a.e. to lam / ∫ τ.

A pure real-analysis ratio lemma

theorem Oseledets.tendsto_div_of_tendsto_div {a r : ℕ → ℝ} {L R : ℝ} (hR : R ≠ 0) (ha : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * a n) Filter.atTop (nhds L)) (hr : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * r n) Filter.atTop (nhds R)) : Filter.Tendsto (fun (n : ℕ) => a n / r n) Filter.atTop (nhds (L / R))

Ratio lemma. If n⁻¹ · a n → L and n⁻¹ · r n → R with R ≠ 0, then the ratio a n / r n → L / R. The common factor n⁻¹ cancels for n ≥ 1, so the ratio is eventually the quotient of the two averages, and Filter.Tendsto.div finishes (the limit denominator is R ≠ 0).

Reconciling roofSum with the Birkhoff sum of the roof

theorem Oseledets.baseIter_natCast {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℕ) (x : X) : baseIter T hτ (↑n) x = (⇑T)^[n] x

The base iterate baseIter (n : ℤ) x, at a natural index n, is the n-th iterate of the base map T applied to x. Proved by induction from the one-step form of suspensionAct.

theorem Oseledets.roofSum_natCast_eq_birkhoffSum {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℕ) (x : X) : roofSum T hτ (↑n) x = birkhoffSum (⇑T) τ n x

Reconciliation. For a natural index n, the suspension roof sum roofSum (n : ℤ) x equals Mathlib's Birkhoff sum birkhoffSum (⇑T) τ n x = ∑_{k<n} τ ((⇑T)^[k] x). Both satisfy F 0 = 0 and F (n+1) = F n + τ ((⇑T)^[n] x) (via roofSum_add_one and baseIter_natCast), so they agree by induction.

The roof average converges a.e. to ∫ τ

theorem Oseledets.tendsto_roofAverage_ae {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic (⇑T) μ) (hτint : MeasureTheory.Integrable τ μ) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * roofSum T hτ (↑n) x) Filter.atTop (nhds (∫ (y : X), τ y ∂μ))

Roof average. When T is ergodic for a probability measure μ and the roof τ is integrable, the roof average n⁻¹ · roofSum n x converges μ-a.e. to the space average ∫ τ ∂μ. This is the ergodic Birkhoff theorem tendsto_birkhoffAverage_ae_integral applied to the roof, after reconciling roofSum with the Birkhoff sum and unfolding birkhoffAverage.

Positivity of the roof integral

theorem Oseledets.integral_roof_pos {X : Type u_1} [MeasurableSpace X] {τ : X → ℝ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (hτint : MeasureTheory.Integrable τ μ) : 0 < ∫ (y : X), τ y ∂μ

Positivity of ∫ τ. A uniform lower bound c ≤ τ with 0 < c on a probability measure forces 0 < ∫ τ ∂μ, since ∫ τ ≥ ∫ c = c · μ univ = c > 0.

The return-time exponent

theorem Oseledets.returnTime_tendsto_exponent {X : Type u_1} [MeasurableSpace X] {d : ℕ} (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {μ : MeasureTheory.Measure X} {A : X → Matrix (Fin d) (Fin d) ℝ} {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 (n : ℕ) => Real.log ‖cocycle A (⇑T) n x‖ / roofSum T hτ (↑n) x) Filter.atTop (nhds (lam / ∫ (y : X), τ y ∂μ))

The return-time exponent. Suppose the base cocycle A has a μ-a.e. log-norm growth rate lam, i.e. n⁻¹ · log ‖cocycle A T n x‖ → lam a.e. (this is the headline output of the discrete Oseledets/Furstenberg–Kesten theorem; it is taken as a hypothesis so the lemma applies to the top exponent, a k-th exponent, or any other rate). Suppose moreover that the roof average converges a.e. to ∫ τ and that ∫ τ ≠ 0. Then the cocycle log-norm rescaled by the return time roofSum n x (the time spent in the suspension after n base steps) converges μ-a.e. to the rescaled exponent lam / ∫ τ.

The proof combines the two a.e. statements pointwise and applies the ratio lemma tendsto_div_of_tendsto_div with a n = log ‖cocycle A T n x‖, r n = roofSum n x, L = lam and R = ∫ τ.