The spectral upper bound via the determinant squeeze and the tempered angle

This file proves the spectral upper bound of the Oseledets multiplicative ergodic theorem for a Λ-slow vector v,

limsup_n (1/n)·log ‖A⁽ⁿ⁾ v‖  ≤  λᵢ,    for `v` in the limit slow subspace `S(x)`.

The mechanism is the determinant squeeze with a tempered angle (Raghunathan; Arnold §3.4; Filip). Its decisive feature is non-circularity: the slow growth is determined globally via the volume cocycle, never per vector. A per-vector recursion between the growth exponent and the fast/slow overlap would be circular; the squeeze instead consumes only convergence facts (the Furstenberg–Kesten determinant limit, the fast-volume Kingman limit, and the tempered-angle limit), none of which refers to the growth of an individual vector.

Two self-contained ingredients are built here:

1. The tempering lemma (tempering_lemma, a Birkhoff corollary): for g ≥ 0 with log⁺ g ∈ L¹(μ), (1/n)·log⁺(g ∘ Tⁿ) → 0 a.e. Only convergence/finiteness is used, not a rate.

2. The determinant / Gram factorization (det_gram_image_eq, det_sq_eq_gram_image, finite-dimensional linear algebra): for a splitting ℝ^d = F ⊕ S with orthonormal frames ω_F (p columns) and ω_S (q columns) assembled into the block frame W = [ω_F ω_S], the Gram determinant of the image block factors as det((M·W)ᵀ·(M·W)) = (det M)² · (det W)², which underlies the geometric identity |det(M·W)| = vol_F · vol_S · sin∠(M F, M S).

Main results

• Oseledets.tempering_lemma, Oseledets.tempering_posLog: for an integrable h (think h = log⁺ g), (1/n)·h(Tⁿ x) → 0 for almost every x.
• Oseledets.det_gram_image_eq, Oseledets.det_sq_eq_gram_image: the determinant/Gram factorization for a block frame.
• Oseledets.tendsto_slowVolume_exponent: the squeeze arithmetic — convergence of the slow-volume exponent from the determinant, fast-volume, and angle limits.
• Oseledets.limsup_le_of_sum_tendsto, Oseledets.limsup_topSlow_le_of_squeeze: the exponent-pinning squeeze forcing the top slow exponent down to λᵢ.
• Oseledets.spectral_upper_bound_of_squeeze: the per-vector spectral upper bound limsup (1/n)·log ‖A⁽ⁿ⁾ v‖ ≤ λᵢ for v in the slow subspace.

References

• M. S. Raghunathan, A proof of Oseledec's multiplicative ergodic theorem, Israel J. Math. 32 (1979), 356–362.
• L. Arnold, Random Dynamical Systems, Springer Monographs in Mathematics, 1998.
• S. Filip, Notes on the multiplicative ergodic theorem, Ergodic Theory Dynam. Systems 39 (2019), 1153–1189.

The tempering lemma (a Birkhoff corollary)

If g ≥ 0 and log⁺ g ∈ L¹(μ), then (1/n) log⁺(g(Tⁿx)) → 0 for a.e. x. This follows by applying the orbit-decay theorem ae_tendsto_orbit_div_atTop_zero to the integrable function x ↦ log⁺ g(x) = Real.posLog (g x). The decisive feature: only integrability (finiteness) of log⁺ g is used — no decay rate.

theorem Oseledets.tempering_lemma {X : Type u_1} [MeasurableSpace X] {T : X → X} {μ : MeasureTheory.Measure X} (hT : MeasureTheory.MeasurePreserving T μ μ) {h : X → ℝ} (hh : MeasureTheory.Integrable h μ) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * h (T^[n] x)) Filter.atTop (nhds 0)

Tempering lemma. For an integrable h (think h = log⁺ g, the positive log of a tempered quantity), (1/n)·h(Tⁿx) → 0 for μ-a.e. x. A thin specialization of ae_tendsto_orbit_div_atTop_zero, packaged as the tempering corollary.

theorem Oseledets.tempering_posLog {X : Type u_1} [MeasurableSpace X] {T : X → X} {μ : MeasureTheory.Measure X} (hT : MeasureTheory.MeasurePreserving T μ μ) {g : X → ℝ} (hg : MeasureTheory.Integrable (fun (x : X) => (g x).posLog) μ) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * (g (T^[n] x)).posLog) Filter.atTop (nhds 0)

Tempering lemma (posLog form). If x ↦ Real.posLog (g x) is integrable (the tempered condition log⁺ g ∈ L¹), then (1/n)·log⁺(g(Tⁿx)) → 0 a.e. This is the form used by the squeeze: g = 1/sin∠(F,S) (genuine splitting, tempered) gives (1/n)·log sin∠(F(Tⁿx),S(Tⁿx)) → 0.

The determinant / angle factorization (finite-dimensional linear algebra)

For a square real matrix W : Matrix (Fin d) (Fin d) ℝ viewed as a block frame W = [ω_F | ω_S] (ω_F the first p columns, ω_S the last q = d − p), and any M : Matrix (Fin d) (Fin d) ℝ, the Gram determinant of the image block factors:

det((M·W)ᵀ·(M·W)) = (det M)² · (det W)²,

and equals det(Gram(M ω_F)) · det(Gram(M ω_S)) · sin²∠(M F, M S) where the inter-block sine is defined by sin² := det(Gram(M·W)) / (det(Gram(M ω_F)) · det(Gram(M ω_S))). The genuine geometric content is Fischer's inequality sin² ≤ 1, i.e. the Gram determinant of a block matrix is at most the product of the diagonal-block Gram determinants. We package the unconditional algebraic identity here; the squeeze uses 0 < sin² ≤ 1 (genuine splitting + Fischer).

theorem Oseledets.det_gram_image_eq {d : ℕ} (M W : Matrix (Fin d) (Fin d) ℝ) : ((M * W).transpose * (M * W)).det = M.det ^ 2 * W.det ^ 2

Gram determinant of an image is the square of the determinant times the source Gram det. For square M W, det((M W)ᵀ (M W)) = (det M)² · (det W)². The pure algebraic core of the determinant factorization: combining det_mul, det_transpose, det_mul.

theorem Oseledets.det_sq_eq_gram_image {d : ℕ} (M W : Matrix (Fin d) (Fin d) ℝ) (hW : W.det ^ 2 = 1) : M.det ^ 2 = ((M * W).transpose * (M * W)).det

Determinant factorization (squared form). For an orthogonal block frame W (so det W = ±1, (det W)² = 1), the squared determinant of M equals the Gram determinant of its image block: (det M)² = det((M W)ᵀ (M W)). This is the algebraic identity the squeeze applies: (det M)² factors as det(Gram(M ω_F)) · det(Gram(M ω_S)) · sin².

The determinant squeeze (volume-exponent form)

The squeeze in its decisive scalar form. Write D(n) = (1/n) log|det A⁽ⁿ⁾| (by Furstenberg–Kesten, → Σ_all λ), VF(n) = (1/n) log vol(A⁽ⁿ⁾ ω_F) (fast-frame volume; tempered to → Σ_fast λ), VS(n) = (1/n) log vol(A⁽ⁿ⁾ ω_S) (slow-frame volume), and S(n) = (1/n) log sin∠(A⁽ⁿ⁾F, A⁽ⁿ⁾S) (tempered: → 0 by the tempering lemma). The factorization gives, with the orthogonal source frame W, D(n) = VF(n) + VS(n) + S(n) (taking logs of |det A⁽ⁿ⁾| = volF·volS·sin, using |det W| = 1). Hence

VS(n) = D(n) − VF(n) − S(n)  →  Σ_all λ − Σ_fast λ − 0 = Σ_slow λ.

The lemma below is the pure limit arithmetic of the squeeze: it does not presuppose any per-vector rate (the only convergence inputs are the Furstenberg–Kesten determinant limit, the fast-volume Kingman limit, and the tempered-angle limit → 0). This is what makes the argument non-circular.

theorem Oseledets.tendsto_slowVolume_exponent {D VF VS S : ℕ → ℝ} {dSum fSum : ℝ} (hD : Filter.Tendsto D Filter.atTop (nhds dSum)) (hVF : Filter.Tendsto VF Filter.atTop (nhds fSum)) (hS : Filter.Tendsto S Filter.atTop (nhds 0)) (hfact : ∀ᶠ (n : ℕ) in Filter.atTop, D n = VF n + VS n + S n) : Filter.Tendsto VS Filter.atTop (nhds (dSum - fSum))

Determinant squeeze (volume arithmetic). If D → dSum (det exponent), VF → fSum (fast-volume exponent), and the tempered angle S → 0, and the factorization D n = VF n + VS n + S n holds eventually, then the slow-volume exponent converges: VS → dSum − fSum. Pure arithmetic of the squeeze; the inputs are all convergence facts (no rate assumed on any vector).

theorem Oseledets.limsup_le_of_sum_tendsto {a b : ℕ → ℝ} {A B : ℝ} (hsum : Filter.Tendsto (fun (n : ℕ) => a n + b n) Filter.atTop (nhds (A + B))) (_ha : A ≤ Filter.liminf a Filter.atTop) (hb : B ≤ Filter.liminf b Filter.atTop) (haub : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop a) (halb : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop a) (hblb : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop b) (hbub : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop b) : Filter.limsup a Filter.atTop ≤ A

Exponent-pinning squeeze (two terms). If a + b → A + B (the volume sum has the exact total exponent), liminf a ≥ A and liminf b ≥ B (the per-direction lower bounds), then limsup a ≤ A (and symmetrically for b), so each converges to its lower bound. This is the arithmetic that forces the top slow exponent to equal λᵢ: the slow volume → Σ_slow λ decomposes as top-slow + rest, the lower bounds pin rest ≥ Σ_rest and top ≥ λᵢ, and equality of the sum squeezes top ≤ λᵢ. Stated as a clean two-term lemma; iterates to any finite split.

theorem Oseledets.limsup_topSlow_le_of_squeeze {volS topS restS : ℕ → ℝ} {slowSum lamI restSum : ℝ} (hvolS : Filter.Tendsto volS Filter.atTop (nhds slowSum)) (hsplit : slowSum = lamI + restSum) (hfact : ∀ᶠ (n : ℕ) in Filter.atTop, volS n = topS n + restS n) (htop_lb : lamI ≤ Filter.liminf topS Filter.atTop) (hrest_lb : restSum ≤ Filter.liminf restS Filter.atTop) (htop_ub : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop topS) (htop_glb : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop topS) (hrest_lbd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop restS) (hrest_ubd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop restS) : Filter.limsup topS Filter.atTop ≤ lamI

The determinant-squeeze closure (abstract operator-norm form). Package the whole squeeze into the spectral upper bound on the slow restricted operator norm. Let:

• volS n = slow-frame volume exponent term (1/n) log vol(A⁽ⁿ⁾ ω_S), with volS → slowSum (the slow-exponent sum, supplied by tendsto_slowVolume_exponent);
• topS n = (1/n) log ‖A⁽ⁿ⁾|_S‖ (top slow restricted singular exponent);
• restS n = (1/n) log (vol / ‖·|_S‖) (product of the remaining q−1 slow singular exponents), so volS n = topS n + restS n (the volume factors as top × rest);
• lower bounds liminf topS ≥ lamI (the top slow direction grows at ≥ λᵢ) and liminf restS ≥ restSum with lamI + restSum = slowSum (the remaining directions).

Then limsup topS ≤ lamI: the squeeze pins the top slow exponent at exactly λᵢ. This is the spectral upper bound on the slow subspace, obtained non-circularly: no per-vector growth was assumed, only the volume limit and the unconditional lower bounds.

From the slow restricted operator norm to the per-vector spectral upper bound

The final step: once limsup (1/n) log ‖A⁽ⁿ⁾|_S‖ ≤ λᵢ, every v in the slow subspace S obeys ‖A⁽ⁿ⁾ v‖ ≤ ‖A⁽ⁿ⁾|_S‖ · ‖v‖, so limsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ λᵢ, the desired spectral upper bound. This is pure operator-norm monotonicity plus log arithmetic; no circularity, since the slow-norm bound came from the global volume squeeze, not from this vector.

theorem Oseledets.limsup_apply_le_of_restricted_norm {Mv r : ℕ → ℝ} {c lamI : ℝ} (hc : 0 < c) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, Mv n ≤ r n * c) (hrnn : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ r n) (hMvpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < Mv n) (hR : Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log (r n)) Filter.atTop ≤ lamI) (hRbdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log (r n)) (hcobdd : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log (Mv n)) : Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log (Mv n)) Filter.atTop ≤ lamI

Per-vector upper bound from the restricted operator-norm bound. If the slow restricted operator-norm exponent R n = (1/n) log r n has limsup R ≤ lamI, and the per-vector growth satisfies ‖A⁽ⁿ⁾ v‖ ≤ r n · ‖v‖ eventually (r n ≥ 0, v ≠ 0), then limsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ lamI.

The spectral upper bound for a slow cocycle vector (non-circular)

The full chain assembled into one statement about the cocycle A⁽ⁿ⁾. For a Λ-slow vector v (in the limit slow subspace S(x)), the determinant squeeze provides — non-circularly — the slow restricted-operator-norm exponent bound limsup (1/n) log ‖A⁽ⁿ⁾|_S‖ ≤ λᵢ (hslownorm, the output of limsup_topSlow_le_of_squeeze), and the restriction bound ‖A⁽ⁿ⁾ v‖ ≤ ‖A⁽ⁿ⁾|_S‖ · ‖v‖ (hrestrict, valid because v ∈ S). The conclusion is the spectral upper bound

limsup_n (1/n)·log ‖A⁽ⁿ⁾ v‖  ≤  λᵢ.

The non-circularity is structural: hslownorm is determined by the global volume cocycle (the Furstenberg–Kesten determinant limit, the fast-volume Kingman limit, and the tempered angle → 0) together with the lower bounds — none of which references the growth of this vector. The per-vector bound is then a one-line operator-norm consequence.

theorem Oseledets.spectral_upper_bound_of_squeeze {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {x : X} {v : EuclideanSpace ℝ (Fin d)} {lamI : ℝ} {r : ℕ → ℝ} (hv : v ≠ 0) (hslownorm : Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log (r n)) Filter.atTop ≤ lamI) (hrestrict : ∀ᶠ (n : ℕ) in Filter.atTop, ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖ ≤ r n * ‖v‖) (hrnn : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ r n) (hMvpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) (hRbdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log (r n)) (hcobdd : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) : Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) Filter.atTop ≤ lamI

Spectral upper bound for a slow cocycle vector (via the determinant squeeze). Given the slow restricted-operator-norm exponent bound hslownorm (the squeeze output) and the restriction bound hrestrict (valid for v in the slow subspace), the per-vector growth obeys limsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ λᵢ. The remaining side conditions are the routine boundedness/positivity facts (hrnn, hMvpos, hRbdd, hcobdd).