Concrete inputs for the determinant-squeeze spectral upper bound

This file wires the concrete cocycle facts into the abstract determinant-squeeze machinery of Oseledets.Lyapunov.ForwardDetSqueeze, producing the spectral upper bound

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

Main results

• Oseledets.SqueezeData: the bundle of concrete cocycle facts along an orbit.
• Oseledets.limsup_slowNorm_le_of_squeezeData: from a SqueezeData, the determinant squeeze bounds the top-slow restricted-norm exponent, limsup (1/n) log ‖A⁽ⁿ⁾|_S‖ ≤ λᵢ.
• Oseledets.spectral_upper_bound_of_squeezeData: from a SqueezeData, the per-vector spectral upper bound limsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ λᵢ.

Implementation notes

The abstract squeeze chain

The abstract chain provided by ForwardDetSqueeze is:

tendsto_slowVolume_exponent (hD, hVF, hS, hfact → slow-volume limit VS → slowSum) → limsup_topSlow_le_of_squeeze (slow-volume limit + hsplit + lower bounds + boundedness → limsup topS ≤ λᵢ) → spectral_upper_bound_of_squeeze (hslownorm + hrestrict + side conditions → the per-vector spectral upper bound).

The concrete cocycle inputs are bundled in SqueezeData, a structure of precisely typed hypotheses — each entry matches the infrastructure lemma that supplies it, so discharging the structure is exactly the remaining concrete work, with no hidden arithmetic. The theorem spectral_upper_bound_of_squeezeData proves the chain is gapless: a SqueezeData alone yields the per-vector spectral upper bound. Boundedness side-conditions are derived where possible from the convergence inputs (a convergent real sequence is bounded above and below, cobounded, etc.), so they are not carried as separate fields.

The fields of SqueezeData

Listed with the lemma that discharges each (see the field docstrings):

• hD — Furstenberg–Kesten det limit (furstenbergKesten_* + det/exterior Kingman).
• hVF — exterior-Kingman fast-volume limit (ExteriorNorm ‖⋀ᵏ‖ = ∏σ + Kingman).
• hS — the tempered angle → 0 (tempering_posLog + L¹-temperedness + Fischer's sin ≤ 1).
• hfact — the determinant/angle factorization (det_sq_eq_gram_image + block-Gram sine).
• htop_lb, hrest_lb — per-direction lower bounds (log_le_liminf_log_cocycle_apply + tendsto_log_singularValue / exists_lam_tendsto_singularValue).
• hrestrict — slow-restriction operator-norm bound (v ∈ S equivariant + op-norm monotonicity).
• hMvpos — strict positivity of the per-vector growth (norm_cocycle_pos applied to v ≠ 0).

References

• L. Arnold, Random dynamical systems, Springer Monographs in Mathematics, Springer (1998).
• D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58.

Boundedness helpers: a convergent real sequence is bounded/cobounded both ways.

These discharge the IsBoundedUnder/IsCoboundedUnder side-conditions of the abstract squeeze lemmas purely from the convergence inputs, so SqueezeData need not carry them as fields.

theorem Oseledets.isBoundedUnder_le_of_tendsto {f : ℕ → ℝ} {a : ℝ} (h : Filter.Tendsto f Filter.atTop (nhds a)) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop f

theorem Oseledets.isBoundedUnder_ge_of_tendsto {f : ℕ → ℝ} {a : ℝ} (h : Filter.Tendsto f Filter.atTop (nhds a)) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop f

theorem Oseledets.isCoboundedUnder_le_of_tendsto {f : ℕ → ℝ} {a : ℝ} (h : Filter.Tendsto f Filter.atTop (nhds a)) : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop f

The concrete cocycle inputs of the determinant squeeze

structure Oseledets.SqueezeData {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (v : EuclideanSpace ℝ (Fin d)) (lamI : ℝ) : Type

SqueezeData A T x v lamI bundles the concrete facts about the cocycle A⁽ⁿ⁾(x) along the orbit of x that feed the determinant squeeze, for a fixed slow vector v in the limit slow subspace S(x) with target top-slow Lyapunov exponent lamI. Each field is typed against the infrastructure lemma that supplies it (see the field docstrings); the boundedness side-conditions are derived (not assumed).

Notation for the sequences (all : ℕ → ℝ):

• D n = (1/n) log|det A⁽ⁿ⁾| — det exponent, → dSum = Σ_all λ (hD).
• VF n = (1/n) log vol(A⁽ⁿ⁾ ω_F) — fast-frame volume exponent, → fSum = Σ_fast λ (hVF).
• VS n = (1/n) log vol(A⁽ⁿ⁾ ω_S) — slow-frame volume exponent (= topS + restS).
• S n = (1/n) log sin∠(A⁽ⁿ⁾F, A⁽ⁿ⁾S) — tempered angle, → 0 (hS).
• topS n = (1/n) log (r n), r n = ‖A⁽ⁿ⁾|_S‖ — top-slow restricted-norm exponent.
• restS n — remaining q−1 slow singular exponents, VS = topS + restS.

• hv : v ≠ 0

  The slow vector is nonzero.

• D : ℕ → ℝ

  Det exponent sequence (1/n) log|det A⁽ⁿ⁾|.

• VF : ℕ → ℝ

  Fast-frame volume exponent sequence.

• VS : ℕ → ℝ

  Slow-frame volume exponent sequence.

• S : ℕ → ℝ

  Tempered-angle exponent sequence.

• topS : ℕ → ℝ

  Top-slow restricted-norm exponent sequence.

• restS : ℕ → ℝ

  Remaining slow-direction exponent sequence.

• r : ℕ → ℝ

  Restricted operator norm r n = ‖A⁽ⁿ⁾|_S‖.

• dSum : ℝ

  Total exponent sum Σ_all λ.

• fSum : ℝ

  Fast exponent sum Σ_fast λ.

• restSum : ℝ

  Rest exponent sum (slow without the top direction).

• hD : Filter.Tendsto self.D Filter.atTop (nhds self.dSum)

  hD — Furstenberg–Kesten det limit: (1/n) log|det A⁽ⁿ⁾| → Σ_all λ. Discharged by furstenbergKesten_* + the det/top-exterior Kingman limit (|det A⁽ⁿ⁾| = ∏ⱼ σⱼ, (1/n)Σ log σⱼ → Σλ).

• hVF : Filter.Tendsto self.VF Filter.atTop (nhds self.fSum)

  hVF — exterior-Kingman fast-volume limit: (1/n) log vol(A⁽ⁿ⁾ ω_F) → Σ_fast λ. Discharged by the exterior-norm identity ‖⋀ᵖ‖ = ∏σ + Kingman (upper), with the fast frame ω_F chosen ≈ the limit top-p singular subspace (band-projector convergence) so the angle defect is tempered (lower).

• hS : Filter.Tendsto self.S Filter.atTop (nhds 0)

  hS — the tempered angle (1/n) log sin∠(A⁽ⁿ⁾F, A⁽ⁿ⁾S) → 0. Discharged by tempering_posLog applied to g = 1/sin∠_splitting (using equivariance A⁽ⁿ⁾S(x) = S(Tⁿx) so the image angle is the splitting angle at Tⁿx), provided log(1/sin∠_splitting) ∈ L¹(μ) (Arnold §3.4; from IntegrableLogNorm A + …A⁻¹), together with Fischer's sin∠ ≤ 1 (so S n ≤ 0, i.e. the posLog captures the whole).

• hfact : ∀ᶠ (n : ℕ) in Filter.atTop, self.D n = self.VF n + self.VS n + self.S n

  hfact — the determinant/angle factorization D n = VF n + VS n + S n. Discharged by det_sq_eq_gram_image (with orthonormal source frame W, |det W| = 1) and the block-Gram definition of sin∠, taking logs of |det A⁽ⁿ⁾| = volF·volS·sin∠.

• hvolfact : ∀ᶠ (n : ℕ) in Filter.atTop, self.VS n = self.topS n + self.restS n

  The slow volume factors into the top-slow restricted norm and the remaining directions: VS n = topS n + restS n. From the singular-value factorization of vol(A⁽ⁿ⁾ ω_S).

• hsplit : self.dSum - self.fSum = lamI + self.restSum

  The slow exponent sum splits as the top-slow exponent lamI plus the rest: (dSum − fSum) = lamI + restSum.

• htop_lb : lamI ≤ Filter.liminf self.topS Filter.atTop

  htop_lb — top-slow per-direction lower bound lamI ≤ liminf topS. Discharged by log_le_liminf_log_cocycle_apply at threshold c = e^{lamI} + tendsto_log_singularValue.

• hrest_lb : self.restSum ≤ Filter.liminf self.restS Filter.atTop

  hrest_lb — remaining-directions lower bound restSum ≤ liminf restS. Discharged by the per-direction singular-value lower bounds for the q−1 non-top slow singular values (exists_lam_tendsto_singularValue).

• htopS_eq : self.topS = fun (n : ℕ) => (↑n)⁻¹ * Real.log (self.r n)

  The top-slow exponent is the normalized log of the restricted operator norm: topS = (1/n) log r.

• htopS_ub : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop self.topS

  The top-slow restricted-norm exponent is bounded above (Furstenberg–Kesten: (1/n) log‖A⁽ⁿ⁾‖ converges, and r n = ‖A⁽ⁿ⁾|_S‖ ≤ ‖A⁽ⁿ⁾‖). Provided as a clean uniform bound.

• htopS_lb : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop self.topS

  The top-slow restricted-norm exponent is bounded below (Furstenberg–Kesten on the inverse cocycle: r n = ‖A⁽ⁿ⁾|_S‖ ≥ 1/‖(A⁽ⁿ⁾)⁻¹‖, whose log-exponent converges by furstenbergKesten_norm_inv). Note: a liminf lower bound alone does NOT give this in a conditionally-complete order, so it is carried explicitly.

• hrestS_ub : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop self.restS

  restS is bounded above (FK: the slow volume is bounded by ‖A⁽ⁿ⁾‖^q, so each exponent term is bounded; equivalently from the convergence of all singular-value exponents).

• hrestS_lb : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop self.restS

  restS is bounded below (FK on the inverse cocycle: singular values stay away from 0).

• hrestrict : ∀ᶠ (n : ℕ) in Filter.atTop, ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖ ≤ self.r n * ‖v‖

  hrestrict — slow-restriction operator-norm bound: ‖A⁽ⁿ⁾ v‖ ≤ r n · ‖v‖. Valid because v ∈ S(x) (equivariant slow subspace) and r n = ‖A⁽ⁿ⁾|_S‖; operator-norm monotonicity.

• hrnn : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ self.r n

  r n ≥ 0 (an operator norm).

• hMvpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖

  hMvpos — strict positivity of the per-vector growth: 0 < ‖A⁽ⁿ⁾ v‖. From v ≠ 0 and det A⁽ⁿ⁾ ≠ 0 (so A⁽ⁿ⁾ is invertible ⇒ A⁽ⁿ⁾ v ≠ 0).

• hcobdd : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖

  The per-vector log-growth sequence is cobounded above (FK: bounded above ⇒ cobounded).

The chain: SqueezeData → limsup topS ≤ λᵢ → spectral upper bound.

theorem Oseledets.limsup_slowNorm_le_of_squeezeData {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {x : X} {v : EuclideanSpace ℝ (Fin d)} {lamI : ℝ} (hsq : SqueezeData A T x v lamI) : Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log (hsq.r n)) Filter.atTop ≤ lamI

The determinant squeeze pins the top-slow exponent. From a SqueezeData, limsup (1/n) log r ≤ λᵢ, where r n = ‖A⁽ⁿ⁾|_S‖ is the slow restricted operator norm. This chains tendsto_slowVolume_exponent (the volume limit VS → dSum − fSum) into limsup_topSlow_le_of_squeeze (the two-term pinning squeeze), with all boundedness side-conditions discharged from the convergence inputs of the data. No per-vector growth information is used, so the bound may feed the per-vector estimate without circularity.

theorem Oseledets.spectral_upper_bound_of_squeezeData {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {x : X} {v : EuclideanSpace ℝ (Fin d)} {lamI : ℝ} (hsq : SqueezeData A T x v lamI) : Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) Filter.atTop ≤ lamI

The per-vector spectral upper bound. The full chain from SqueezeData: for a slow vector v in the limit slow subspace S(x), the determinant squeeze yields

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

All hypotheses of spectral_upper_bound_of_squeeze are discharged from the data (the slow-norm limsup bound from limsup_slowNorm_le_of_squeezeData, the restriction bound, positivity, and the boundedness side-conditions, the last derived from the slow-norm bound).