Documentation

Oseledets.Lyapunov.ForwardUpperBound

The Lyapunov spectral upper bound via a two-term band split #

This file proves the spectral upper bound of the multiplicative ergodic theorem along Viana's one-sided route: a two-term split of the cocycle quadratic form against the band projector Pₙ = bandProjector A T 𝟙_{(c,∞)} n x at threshold c = e^{λᵢ} (the fast singular-block projector of qpow A T n x).

Adding the two halves yields the master inequality ‖A⁽ⁿ⁾ v‖² ≤ ‖A⁽ⁿ⁾‖²·‖Pₙ v‖² + c^{2n}·‖v‖², from which the spectral upper bound limsup (1/n) log‖A⁽ⁿ⁾ v‖ ≤ λᵢ follows, conditional on the single angle input limsup (1/n) log(‖A⁽ⁿ⁾‖·‖Pₙ v‖) ≤ λᵢ. Via the Furstenberg–Kesten top exponent (1/n)log‖A⁽ⁿ⁾‖ → λ₁, that angle input is in turn equivalent to the tilt-decay residual limsup (1/n) log‖Pₙ v‖ ≤ λᵢ − λ₁.

Main results #

Implementation notes #

A naive per-overlap recursion is circular: slow growth g ≤ λᵢ and small overlaps oⱼ ≤ g − λⱼ (Cauchy–Schwarz) compose vacuously to g ≤ g. The two-term split sidesteps the per-overlap recursion entirely: the slow half (inner_slow_band_le) gives λᵢ unconditionally — it never references an overlap, only the spectral ceiling c of the slow Gram block. The growth is thereby reduced to a single scalar quantity, the fast-band projection ‖Pₙ v‖, whose decay (htilt) is a genuine slow–fast angle estimate about the projector sequence, independent of g; there is no feedback loop.

The one non-elementary input is htilt: limsup (1/n) log‖Pₙ v‖ ≤ λᵢ − λ₁ for the limit-slow vector v (P v = 0, P = limₙ Pₙ), the slow–fast angle decay at the full multi-gap rate λᵢ − λ₁. It is kept as an explicit hypothesis in this file. The summability estimate summable_norm_bandProjector_succ_sub (in Oseledets.Lyapunov.OseledetsLimit) supplies ‖Pₙ₊₁ − Pₙ‖ summability at the nearest-gap rate λᵢ − λ_{i−1}; upgrading it to the full rate is a multi-gap telescope carried out elsewhere in the library.

References #

The slow-band growth bound (the clean half of the split) #

A⁽ⁿ⁾ restricted to the SLOW Gram-eigenspace (singular values ≤ c) has operator norm ≤ c. Concretely, for the complementary band projector Q_n = I - P_n (projection onto eigenvalues ≤ c of qpow), ‖A⁽ⁿ⁾ Q_n v‖² ≤ c^{2n} ‖Q_n v‖² ≤ c^{2n} ‖v‖². This needs NO angle/tilt estimate.

theorem Oseledets.inner_slow_band_le {X : Type u_1} [MeasurableSpace X] {d : } [NeZero d] (A : XMatrix (Fin d) (Fin d) ) (T : XX) {n : } (hn : 1 n) (x : X) {c : } (hc : 0 c) (w : EuclideanSpace (Fin d)) :
inner ((Matrix.toEuclideanLin (cfc (fun (t : ) => t ^ (2 * n) * (1 - (Set.Ioi c).indicator 1 t)) (qpow A T n x))) w) w c ^ (2 * n) * w ^ 2

Slow-band upper bound. For c ≥ 0, the SLOW quadratic form of the cocycle (the part of ‖A⁽ⁿ⁾ w‖² supported on qpow-eigenvalues ≤ c) is ≤ c^{2n} ‖w‖². Formally: applying the gram quadratic form to the complementary band vector w with P_n w = 0. We package it via the function g(t) = t^{2n}·(1 - χ(t)) whose cfc is the slow part of gram.

theorem Oseledets.rpow_mem_spectrum_qpow_le {X : Type u_1} [MeasurableSpace X] {d : } [NeZero d] (A : XMatrix (Fin d) (Fin d) ) (T : XX) {n : } (hn : 1 n) (x : X) {t : } (ht : t spectrum (qpow A T n x)) :
t ^ (2 * n) cocycle A T n x ^ 2

Spectral bound on qpow. Every t in the spectrum of qpow A T n x satisfies t ^ (2n) ≤ ‖A⁽ⁿ⁾‖². (t^{2n} is a gram eigenvalue, gram = cocycleᵀ·cocycle, and a PSD eigenvalue is ≤ ‖gram‖ ≤ ‖cocycleᵀ‖·‖cocycle‖ = ‖cocycle‖².)

The fast-band bound (the angle term) #

theorem Oseledets.inner_fast_band_le {X : Type u_1} [MeasurableSpace X] {d : } [NeZero d] (A : XMatrix (Fin d) (Fin d) ) (T : XX) {n : } (hn : 1 n) (x : X) (c : ) (w : EuclideanSpace (Fin d)) :
inner ((Matrix.toEuclideanLin (cfc (fun (t : ) => t ^ (2 * n) * (Set.Ioi c).indicator 1 t) (qpow A T n x))) w) w cocycle A T n x ^ 2 * (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi c).indicator 1) n x)) w ^ 2

Fast-band upper bound. The fast quadratic form of the cocycle (part of ‖A⁽ⁿ⁾ w‖² supported on qpow-eigenvalues > c) is ≤ ‖A⁽ⁿ⁾‖² · ‖P_n w‖², where P_n w = bandProjector of the fast band applied to w. The eigenvalues t^{2n} on the fast band are ≤ ‖A⁽ⁿ⁾‖² (rpow_mem_spectrum_qpow_le), so cfc(t^{2n}χ) ⪯ ‖A⁽ⁿ⁾‖²·cfc(χ) (PSD), and ⟪cfc(χ)w,w⟫ = ‖P_n w‖² (self-adjoint idempotent).

The master inequality: Viana's two-term split #

‖A⁽ⁿ⁾ v‖² ≤ ‖A⁽ⁿ⁾‖² · ‖P_n v‖² + c^{2n} · ‖v‖². The first term is the FAST (angle) part; the second is the SLOW part (clean).

theorem Oseledets.norm_sq_cocycle_apply_le_split {X : Type u_1} [MeasurableSpace X] {d : } [NeZero d] (A : XMatrix (Fin d) (Fin d) ) (T : XX) {n : } (hn : 1 n) (x : X) {c : } (hc : 0 c) (v : EuclideanSpace (Fin d)) :
(Matrix.toEuclideanLin (cocycle A T n x)) v ^ 2 cocycle A T n x ^ 2 * (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi c).indicator 1) n x)) v ^ 2 + c ^ (2 * n) * v ^ 2

Master inequality (Viana's split). For c ≥ 0: ‖A⁽ⁿ⁾ v‖² ≤ ‖A⁽ⁿ⁾‖² · ‖P_n v‖² + c^{2n} · ‖v‖², where P_n is the fast band projector (bandProjector of (c,∞)).

The assembly: master inequality + angle input ⟹ spectral upper bound #

The slow term contributes λᵢ for free. The fast term ‖A⁽ⁿ⁾‖·‖P_n v‖ is the irreducible ANGLE/tilt input: its normalized-log limsup must be ≤ λᵢ. Given that single hypothesis, the spectral upper bound limsup (1/n)log‖A⁽ⁿ⁾v‖ ≤ λᵢ follows.

theorem Oseledets.limsup_log_cocycle_apply_le_of_angle {X : Type u_1} [MeasurableSpace X] {d : } [NeZero d] (A : XMatrix (Fin d) (Fin d) ) (T : XX) (x : X) {v : EuclideanSpace (Fin d)} (hv : v 0) {lamI : } (hangle : Filter.limsup (fun (n : ) => (↑n)⁻¹ * Real.log (cocycle A T n x * (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v)) Filter.atTop lamI) (hanglebdd : Filter.IsBoundedUnder (fun (x1 x2 : ) => x1 x2) Filter.atTop fun (n : ) => (↑n)⁻¹ * Real.log (cocycle A T n x * (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v)) (hpos : ∀ᶠ (n : ) in Filter.atTop, 0 < (Matrix.toEuclideanLin (cocycle A T n x)) v) (hcobdd : Filter.IsCoboundedUnder (fun (x1 x2 : ) => x1 x2) Filter.atTop fun (n : ) => (↑n)⁻¹ * Real.log (Matrix.toEuclideanLin (cocycle A T n x)) v) :

Spectral upper bound (assembled, conditional on the angle input). For v ≠ 0 and threshold c = exp λᵢ, if the fast term satisfies the angle bound limsup (1/n) log (‖A⁽ⁿ⁾‖ · ‖P_n v‖) ≤ λᵢ, then limsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ λᵢ.

This is the two-term split: the slow band gives λᵢ unconditionally (norm_sq_cocycle_apply_le_split, the c^{2n}‖v‖² term); the fast band is controlled by the angle hypothesis hangle. The only genuinely non-elementary input is hangle (the slow–fast tempering/angle decay of ‖P_n v‖).

The angle hypothesis from a tilt-decay rate on ‖P_n v‖ #

The angle input hangle of limsup_log_cocycle_apply_le_of_angle is the slow–fast tempering decay limsup (1/n) log (‖A⁽ⁿ⁾‖ · ‖P_n v‖) ≤ λᵢ. With the Furstenberg–Kesten top exponent (1/n) log ‖A⁽ⁿ⁾‖ → λ₁, this is equivalent to the tilt-decay rate limsup (1/n) log ‖P_n v‖ ≤ λᵢ − λ₁. This section packages that equivalence: the genuine non-elementary content is exactly the tilt-decay htilt.

theorem Oseledets.angle_of_tilt_decay {X : Type u_1} {d : } [NeZero d] (A : XMatrix (Fin d) (Fin d) ) (T : XX) (x : X) {v : EuclideanSpace (Fin d)} {lamI lam1 : } (htop : Filter.Tendsto (fun (n : ) => (↑n)⁻¹ * Real.log cocycle A T n x) Filter.atTop (nhds lam1)) (htiltbdd : Filter.IsBoundedUnder (fun (x1 x2 : ) => x1 x2) Filter.atTop fun (n : ) => (↑n)⁻¹ * Real.log (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v) (htilt : Filter.limsup (fun (n : ) => (↑n)⁻¹ * Real.log (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v) Filter.atTop lamI - lam1) (htiltcob : Filter.IsCoboundedUnder (fun (x1 x2 : ) => x1 x2) Filter.atTop fun (n : ) => (↑n)⁻¹ * Real.log (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v) (hsumcob : Filter.IsCoboundedUnder (fun (x1 x2 : ) => x1 x2) Filter.atTop fun (n : ) => (↑n)⁻¹ * Real.log (cocycle A T n x * (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v)) (hcnpos : ∀ᶠ (n : ) in Filter.atTop, 0 < cocycle A T n x) (hPvpos : ∀ᶠ (n : ) in Filter.atTop, 0 < (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v) :

Angle from tilt-decay. If the Furstenberg–Kesten top exponent is λ₁ (htop) and the fast-band projection ‖P_n v‖ decays at the tempering rate limsup (1/n) log ‖P_n v‖ ≤ λᵢ − λ₁ (htilt), then the angle hypothesis of limsup_log_cocycle_apply_le_of_angle holds.

The spectral upper bound from the tilt-decay residual #

Assembling the two-term split (limsup_log_cocycle_apply_le_of_angle) with the Furstenberg–Kesten reduction (angle_of_tilt_decay) yields the spectral upper bound in lambdaBar form: for a Λ-slow vector v (its top fast-band projection decays at the tempering rate), lambdaBar A T x v ≤ λᵢ.

The single genuinely non-elementary hypothesis is htilt: the slow–fast tempering/angle decay limsup (1/n) log ‖P_n v‖ ≤ λᵢ − λ₁. Everything else (the slow-band c^{2n} bound, the Furstenberg–Kesten top exponent, the limsup arithmetic) is supplied here unconditionally.

theorem Oseledets.lambdaBar_le_of_tilt_decay {X : Type u_1} [MeasurableSpace X] {d : } [NeZero d] (A : XMatrix (Fin d) (Fin d) ) (T : XX) (x : X) {v : EuclideanSpace (Fin d)} (hv : v 0) {lamI lam1 : } (htop : Filter.Tendsto (fun (n : ) => (↑n)⁻¹ * Real.log cocycle A T n x) Filter.atTop (nhds lam1)) (htiltbdd : Filter.IsBoundedUnder (fun (x1 x2 : ) => x1 x2) Filter.atTop fun (n : ) => (↑n)⁻¹ * Real.log (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v) (htilt : Filter.limsup (fun (n : ) => (↑n)⁻¹ * Real.log (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v) Filter.atTop lamI - lam1) (htiltcob : Filter.IsCoboundedUnder (fun (x1 x2 : ) => x1 x2) Filter.atTop fun (n : ) => (↑n)⁻¹ * Real.log (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v) (hsumcob : Filter.IsCoboundedUnder (fun (x1 x2 : ) => x1 x2) Filter.atTop fun (n : ) => (↑n)⁻¹ * Real.log (cocycle A T n x * (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v)) (hcnpos : ∀ᶠ (n : ) in Filter.atTop, 0 < cocycle A T n x) (hPvpos : ∀ᶠ (n : ) in Filter.atTop, 0 < (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v) (hangbdd : Filter.IsBoundedUnder (fun (x1 x2 : ) => x1 x2) Filter.atTop fun (n : ) => (↑n)⁻¹ * Real.log (cocycle A T n x * (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (Real.exp lamI)).indicator 1) n x)) v)) (hcocpos : ∀ᶠ (n : ) in Filter.atTop, 0 < (Matrix.toEuclideanLin (cocycle A T n x)) v) (hcobdd : Filter.IsCoboundedUnder (fun (x1 x2 : ) => x1 x2) Filter.atTop fun (n : ) => (↑n)⁻¹ * Real.log (Matrix.toEuclideanLin (cocycle A T n x)) v) :
lambdaBar A T x v lamI

The spectral upper bound, lambdaBar form. For a nonzero v, the Furstenberg–Kesten top exponent λ₁ (htop), and the tilt-decay residual htilt (limsup (1/n) log ‖P_n v‖ ≤ λᵢ − λ₁, the slow–fast angle estimate), together with the routine boundedness/positivity side conditions, the growth exponent obeys the spectral upper bound:

lambdaBar A T x v  ≤  λᵢ.

Equivalently limsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ λᵢ. The slow vector hypothesis P v = 0 (v orthogonal to the limit fast singular subspace) is what makes htilt hold; reducing htilt to P v = 0 is the residual multi-gap tilt-decay (see the module docstring).