The band-projector increment bound and convergence

The single-step band-projector increment bound and its consequences: the abstract Pythagoras / sin-Θ assembly, the Plücker det-Gram wiring of the cocycle data, and the geometric summability of the increments that yields a.e. convergence of the band projectors at a spectral gap.

Main definitions

• Oseledets.lamCocycle, Oseledets.pluckerTopVec — the per-step exponent cocycle and the Plücker (wedge) top vector carrying the gap data.
• Oseledets.bCocycle, Oseledets.stepHypCocycle — the increment-bound and step cocycles.

Main results

• Oseledets.norm_bandProjector_succ_sub_le, Oseledets.norm_bandProjector_succ_sub_le_cocycle — the single-step band-projector increment bound, abstract and cocycle forms.
• Oseledets.exists_tendsto_bandProjector — a.e. convergence of the band projectors.
• Oseledets.tendsto_bandProjector_of_gap — convergence at a genuine spectral gap.

The band-projector increment bound (assembly)

The single-step band-projector increment bound norm_bandProjector_succ_sub_le — the convergence point of the refined off-diagonal sin-Θ route. It threads:

• the Frobenius back-transport ExteriorNorm.norm_proj_sub_le_wedge (‖UUᵀ − VVᵀ‖² ≤ 2k(1 − det(UᵀV)²)),
• the Plücker det-Gram identity ExteriorNorm.inner_hodgeTrivialization_ιMulti (det(UᵀV) = ⟪wedge U, wedge V⟫),
• the refined off-diagonal sin-Θ core offdiag_sin_le_residual_div_gap (‖vt − ⟪vt,v₀⟫v₀‖ ≤ residual/(μ₀ − ν)),
• the cocycle off-diagonal numerator ExteriorNorm.norm_offdiag_residual_compound_le and the ν-ceiling ExteriorNorm.perturbed_compound_gram_ceiling,
• the Plücker eigenpair ExteriorNorm.plucker_eigenpair_ceiling_standard.

The abstract Pythagoras-to-sin bound and the abstract assembly of steps 1–4 (norm_proj_sub_le_residual_div_gap), followed by the cocycle data.

theorem Oseledets.norm_sub_proj_sq_eq_one_sub_inner_sq {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v₀ vt : E} (hv₀ : ‖v₀‖ = 1) (hvt : ‖vt‖ = 1) : ‖vt - inner ℝ vt v₀ • v₀‖ ^ 2 = 1 - inner ℝ vt v₀ ^ 2

Pythagoras gap, unit form. For unit vectors vt, v₀ in a real inner product space, the squared sine of the angle equals one minus the squared cosine: ‖vt − ⟪vt, v₀⟫ v₀‖² = 1 − ⟪vt, v₀⟫².

theorem Oseledets.norm_proj_sub_le_residual_div_gap {d : ℕ} [NeZero d] {k : ℕ} (U V : Matrix (Fin d) (Fin k) ℝ) (hU : U.transpose * U = 1) (hV : V.transpose * V = 1) {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {C : E →ₗ[ℝ] E} {μ₀ ν : ℝ} {v₀ vt : E} (hv₀ : ‖v₀‖ = 1) (hvtnorm : ‖vt‖ = 1) (hev : C vt = μ₀ • vt) (hgap : ν < μ₀) (hν : ∀ (w : E), inner ℝ w v₀ = 0 → inner ℝ (C w) w ≤ ν * ‖w‖ ^ 2) (hdet : (U.transpose * V).det = inner ℝ vt v₀) : ‖U * U.transpose - V * V.transpose‖ ≤ √(2 * ↑k) * (‖C v₀ - inner ℝ (C v₀) v₀ • v₀‖ / (μ₀ - ν))

Abstract assembly (steps 1–4). Combines the Frobenius back-transport, the Plücker det-Gram identity, the Pythagoras gap, and the refined off-diagonal sin-Θ core into a single per-step projector-increment bound. Given orthonormal frames U, V (UᵀU = VᵀV = 1), an abstract symmetric operator C (the perturbed compound Gram) with top unit eigenvector vt (eigenvalue μ₀) and ν-ceiling on v₀^⊥, a reference unit eigenline v₀, and the det-Gram/wedge identification det(UᵀV) = ⟪vt, v₀⟫, the band-projector increment obeys ‖UUᵀ − VVᵀ‖ ≤ √(2k) · ‖C v₀ − ⟪C v₀, v₀⟫ v₀‖ / (μ₀ − ν).

theorem Oseledets.numerator_div_gap_le {cM cB cBi r denom : ℝ} (hcM : 0 ≤ cM) (_hcB : 0 ≤ cB) (_hcBi : 0 ≤ cBi) (hr : 0 ≤ r) (hκr : (cB * cBi) ^ 2 * r ^ 2 < 1) (hdenom : cM ^ 2 / cBi ^ 2 * (1 - (cB * cBi) ^ 2 * r ^ 2) ≤ denom) (_hdenompos : 0 < denom) (hcBipos : 0 < cBi) : cM * (cM * r) * cB ^ 2 / denom ≤ (cB * cBi) ^ 2 * r / (1 - (cB * cBi) ^ 2 * r ^ 2)

Scalar simplification. The off-diagonal numerator over the gap denominator collapses to the κ²·r/(1 − κ²r²) shape that drives the root test. With the compound-norm abbreviations cM = ‖compound k Mₙ‖, cB = ‖compound k B‖, cBi = ‖compound k B⁻¹‖, κ = cB·cBi, r = σₖ/σₖ₋₁, the off-diagonal numerator is cM·√μ₁·cB² with μ₁ = cM²·r² (so √μ₁ = cM·r, using cM ≥ 0, r ≥ 0), and a lower bound on the gap μ̃₀ − ν ≥ cM²/cBi² · (1 − κ²r²). When κ²r² < 1 the ratio numerator / (μ̃₀ − ν) ≤ κ²·r / (1 − κ²r²). This is the constant whose (1/n)·log limit is λₖ − λₖ₋₁ < 0.

The per-step band-projector increment bound (cocycle target)

The convergence point of the refined off-diagonal sin-Θ route. With Mₙ = cocycle A T n x, B = A(T^[n] x) the one-step left factor (so cocycle A T (n+1) x = B * Mₙ), σ = (toEuclideanLin Mₙ).singularValues, r = σₖ/σₖ₋₁, and κ = ‖compound k B‖·‖compound k B⁻¹‖, the band projectors at consecutive steps satisfy ‖Pₙ₊₁ − Pₙ‖ ≤ √(2k)·κ²r/(1 − κ²r²) in the EVENTUAL regime κ²r² < 1.

The proof composes the pieces:

• bandProjector_indicator_eq_frame (n, n+1) → Pₙ = UUᵀ, Pₙ₊₁ = VVᵀ, UᵀU = VᵀV = 1;
• ExteriorNorm.norm_offdiag_residual_compound_le → off-diagonal numerator ‖C v₀ − ⟪C v₀,v₀⟫v₀‖ ≤ cM·√μ₁·cB²;
• ExteriorNorm.perturbed_compound_gram_ceiling → the ν = μ₁·cB² ceiling on v₀^⊥;
• offdiag_sin_le_residual_div_gap (via the abstract assembly norm_proj_sub_le_residual_div_gap) → ‖Pₙ₊₁ − Pₙ‖ ≤ √(2k)·(numerator/(μ̃₀ − ν));
• numerator_div_gap_le → the final κ²r/(1 − κ²r²) shape.

Eventual-regime caveat. The denominator positivity μ̃₀ − ν > 0 holds only for r < 1/κ, which is a tail property along the orbit (since r → 0 geometrically while κ is tempered); hence the bound is stated under the explicit regime hypothesis hev.

Threaded gap hypotheses. To keep the statement's elaboration cheap (the ⋀^k-finrank-indexed Euclidean types are extremely costly to whnf repeatedly), the perturbed compound Gram operator is kept ABSTRACT here: C : EuclideanSpace ℝ (Fin N) →ₗ[ℝ] _ with N the wedge dimension, v₀/vt the reference / perturbed top eigenvectors, and cM, cB, cBi the abstract compound operator norms ‖compound k Mₙ‖, ‖compound k B‖, ‖compound k B⁻¹‖. The cocycle instantiation — N = finrank(⋀^k ℝᵈ), C = adjoint Gₙ₊₁ ∘ₗ Gₙ₊₁, the eigenpair/ceiling data from ExteriorNorm.plucker_eigenpair_ceiling_standard (at gram A T n x, gram A T (n+1) x, identified with the compound Gram via ExteriorNorm.compoundMatrix_gram), the off-diagonal numerator ExteriorNorm.norm_offdiag_residual_compound_le, the ν = μ₁·cB² ceiling ExteriorNorm.perturbed_compound_gram_ceiling, and the det-Gram / wedge↔frame identification det(UᵀV) = ⟪vt, v₀⟫ (via ExteriorNorm.inner_hodgeTrivialization_ιMulti) — is pure bookkeeping with no further analytic content; it is threaded as hypotheses here because the band-projector frame ↔ Plücker eigenvector bridge and the rank-1 lower bound μ̃₀ ≥ cM²/cBi² are discharged separately, and the ⋀^k-type instantiation times out the elaborator at this granularity.

Eventual-regime caveat. The denominator positivity μ̃₀ − ν > 0 holds only for r < 1/κ, which is a tail property along the orbit (since r → 0 geometrically while κ is tempered); hence the bound is stated under the explicit regime hypotheses hgap/hκr.

theorem Oseledets.norm_bandProjector_succ_sub_le {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {c : ℝ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) {k : ℕ} (n : ℕ) (x : X) (U V : Matrix (Fin d) (Fin k) ℝ) (hU : U.transpose * U = 1) (hV : V.transpose * V = 1) (hPn : bandProjector A T ((Set.Ioi c).indicator 1) n x = U * U.transpose) (hPn1 : bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x = V * V.transpose) {N : ℕ} {C : EuclideanSpace ℝ (Fin N) →ₗ[ℝ] EuclideanSpace ℝ (Fin N)} {v₀ vt : EuclideanSpace ℝ (Fin N)} (hv₀ : ‖v₀‖ = 1) (hvt : ‖vt‖ = 1) {μ₀ μ₁ : ℝ} (hev : C vt = μ₀ • vt) {cM cB cBi r : ℝ} (hcM : 0 ≤ cM) (hcB : 0 ≤ cB) (hr : 0 ≤ r) (hnum : ‖C v₀ - inner ℝ (C v₀) v₀ • v₀‖ ≤ cM * (cM * r) * cB ^ 2) (hceil : ∀ (z : EuclideanSpace ℝ (Fin N)), inner ℝ z v₀ = 0 → inner ℝ (C z) z ≤ μ₁ * cB ^ 2 * ‖z‖ ^ 2) (hdet : (U.transpose * V).det = inner ℝ vt v₀) (hμ₀lb : cM ^ 2 / cBi ^ 2 * (1 - (cB * cBi) ^ 2 * r ^ 2) ≤ μ₀ - μ₁ * cB ^ 2) (hgap : μ₁ * cB ^ 2 < μ₀) (hκr : (cB * cBi) ^ 2 * r ^ 2 < 1) (hcBipos : 0 < cBi) : ‖bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x - bandProjector A T ((Set.Ioi c).indicator 1) n x‖ ≤ √(2 * ↑k) * ((cB * cBi) ^ 2 * r / (1 - (cB * cBi) ^ 2 * r ^ 2))

The cocycle instantiation of the per-step band-projector bound

This instantiation discharges the abstract hypotheses of norm_bandProjector_succ_sub_le from the cocycle exterior-power machinery, using the sorted Gram eigenframes (bandProjector_indicator_eq_sortedTopFrame). With Mₙ = cocycle A T n x, B = A(T^[n] x) (so cocycle A T (n+1) x = B · Mₙ), the perturbed compound Gram operator Cₙ₊₁ = adjoint Gₙ₊₁ ∘ₗ Gₙ₊₁ (Gₙ₊₁ = toEuclideanLin (compoundMatrix k (B·Mₙ))), the Plücker top eigenvectors v₀ = ⋀{u₀…u_{k-1}}(gram n), vt = ⋀{u'₀…u'_{k-1}}(gram (n+1)):

• hev from ExteriorNorm.plucker_eigenpair_ceiling_standard' at gram (n+1) (via compound_gram_op_eq);
• hnum from ExteriorNorm.norm_offdiag_residual_compound_le (with √μ₁ = cM·r);
• hceil from ExteriorNorm.perturbed_compound_gram_ceiling;
• hdet from ExteriorNorm.det_transpose_mul_eq_inner_onbTriv + colE_sortedTopFrame;
• hPn, hPn1 from bandProjector_indicator_eq_sortedTopFrame;
• the scalar regime hypotheses (hμ₀lb, hgapμ, hκr, hcBipos) threaded as inputs (the EVENTUAL κ²r² < 1 regime — discharged a.e. by the unconditional root-test convergence layer below).

theorem Oseledets.compound_gram_op_eq {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) (k : ℕ) : LinearMap.adjoint (Matrix.toEuclideanLin (ExteriorNorm.compoundMatrix k (cocycle A T n x))) ∘ₗ Matrix.toEuclideanLin (ExteriorNorm.compoundMatrix k (cocycle A T n x)) = Matrix.toEuclideanLin (ExteriorNorm.compoundMatrix k (gram A T n x))

The compound Gram operator of the cocycle is toEuclideanLin (compoundMatrix k (gram)). adjoint Gₙ ∘ₗ Gₙ = toEuclideanLin (compoundMatrix k (gram A T n x)), where Gₙ = toEuclideanLin (compoundMatrix k (cocycle A T n x)). Via compoundMatrix_gram and the matrix adjoint identity toEuclideanLin (Nᴴ) = (toEuclideanLin N).adjoint (no NeZero on the wedge dimension needed).

theorem Oseledets.norm_compound_apply_pluckerVec {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) {k : ℕ} (v₀ : EuclideanSpace ℝ (Fin (Module.finrank ℝ ↥(⋀[ℝ]^k (EuclideanSpace ℝ (Fin d)))))) (hv₀ : ‖v₀‖ = 1) (hev : (Matrix.toEuclideanLin (ExteriorNorm.compoundMatrix k (gram A T n x))) v₀ = (∏ i ∈ Finset.range k, (Matrix.toEuclideanLin (cocycle A T n x)).singularValues i ^ 2) • v₀) : ‖(Matrix.toEuclideanLin (ExteriorNorm.compoundMatrix k (cocycle A T n x))) v₀‖ = ‖ExteriorNorm.compoundMatrix k (cocycle A T n x)‖

The Plücker top eigenvector achieves the compound operator norm. If v₀ is a unit Plücker top eigenvector of Cₙ = adjoint Gₙ ∘ₗ Gₙ (eigenvalue ∏_{i<k} σᵢ²), then ‖Gₙ v₀‖ = ‖compound Mₙ‖ (= ∏_{i<k} σᵢ = √μ₀). This htop hypothesis of ExteriorNorm.norm_offdiag_residual_compound_le.

noncomputable def Oseledets.lamCocycle {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) : ℕ → ℝ

The sorted-Gram-eigenvalue family lam i = σᵢ² of the cocycle iterate (= eigenvalues₀ (gram), antitone, nonneg). The lam consumed by ExteriorNorm.plucker_eigenpair_ceiling_standard'.

Equations

• Oseledets.lamCocycle A T n x i = (Matrix.toEuclideanLin (Oseledets.cocycle A T n x)).singularValues i ^ 2

theorem Oseledets.lamCocycle_antitone {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) : Antitone (lamCocycle A T n x)

theorem Oseledets.lamCocycle_nonneg {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) (i : ℕ) : 0 ≤ lamCocycle A T n x i

theorem Oseledets.lamCocycle_eigenpair {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) (i : Fin (Fintype.card (Fin d))) : (Matrix.toEuclideanLin (gram A T n x)) ((sortedGramEigenbasis A T n x) i) = lamCocycle A T n x ↑i • (sortedGramEigenbasis A T n x) i

noncomputable def Oseledets.pluckerTopVec {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) {k : ℕ} (hkd : k ≤ Fintype.card (Fin d)) : EuclideanSpace ℝ (Fin (Module.finrank ℝ ↥(⋀[ℝ]^k (EuclideanSpace ℝ (Fin d)))))

The Plücker top eigenvector of Cₙ: the Hodge-trivialized wedge onbTriv basisFun (⋀ {u₀…u_{k-1}}) of the sorted top-k Gram eigenvectors. This is the v₀ shared by ExteriorNorm.plucker_eigenpair_ceiling_standard' and ExteriorNorm.det_transpose_mul_eq_inner_onbTriv (via colE_sortedTopFrame).

Equations

• One or more equations did not get rendered due to their size.

theorem Oseledets.plucker_cocycle_data {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) {k : ℕ} (hk1 : 1 ≤ k) (hkd : k ≤ Fintype.card (Fin d)) (hgap : lamCocycle A T n x k < lamCocycle A T n x (k - 1)) : ‖pluckerTopVec A T n x hkd‖ = 1 ∧ (Matrix.toEuclideanLin (ExteriorNorm.compoundMatrix k (gram A T n x))) (pluckerTopVec A T n x hkd) = (∏ i ∈ Finset.range k, lamCocycle A T n x i) • pluckerTopVec A T n x hkd ∧ (∏ i ∈ Finset.range (k - 1), lamCocycle A T n x i) * lamCocycle A T n x k < ∏ i ∈ Finset.range k, lamCocycle A T n x i ∧ ∀ (w : EuclideanSpace ℝ (Fin (Module.finrank ℝ ↥(⋀[ℝ]^k (EuclideanSpace ℝ (Fin d)))))), inner ℝ w (pluckerTopVec A T n x hkd) = 0 → inner ℝ ((Matrix.toEuclideanLin (ExteriorNorm.compoundMatrix k (gram A T n x))) w) w ≤ (∏ i ∈ Finset.range (k - 1), lamCocycle A T n x i) * lamCocycle A T n x k * ‖w‖ ^ 2

The Plücker eigenpair/ceiling data for the cocycle compound Gram operator. Specialization of ExteriorNorm.plucker_eigenpair_ceiling_standard' to gram A T n x with the sorted eigenbasis and lam = σ²: the top eigenvector pluckerTopVec is a unit vector, an eigenvector of toEuclideanLin (compoundMatrix k (gram)) with eigenvalue ∏_{i<k} σᵢ², the gap ∏_{i<k-1}σᵢ²·σₖ² < ∏_{i<k}σᵢ² holds, and the second-eigenvalue ceiling on its orthocomplement.

theorem Oseledets.norm_bandProjector_succ_sub_le_cocycle {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (hA : ∀ (x : X), (A x).det ≠ 0) (n : ℕ) (x : X) (c : ℝ) {k : ℕ} (hk1 : 1 ≤ k) (hkd : k ≤ Fintype.card (Fin d)) (htopN : ∀ (j : Fin k), c < ⋯.eigenvalues₀ ⟨↑j, ⋯⟩) (hcountN : Fintype.card { i : Fin d // c < ⋯.eigenvalues i } = k) (htopN1 : ∀ (j : Fin k), c < ⋯.eigenvalues₀ ⟨↑j, ⋯⟩) (hcountN1 : Fintype.card { i : Fin d // c < ⋯.eigenvalues i } = k) (hgapN : lamCocycle A T n x k < lamCocycle A T n x (k - 1)) (hgapN1 : lamCocycle A T (n + 1) x k < lamCocycle A T (n + 1) x (k - 1)) (hcBipos : 0 < ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))⁻¹‖) (hμ₀lb : ‖ExteriorNorm.compoundMatrix k (cocycle A T n x)‖ ^ 2 / ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))⁻¹‖ ^ 2 * (1 - (‖ExteriorNorm.compoundMatrix k (A (T^[n] x))‖ * ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))⁻¹‖) ^ 2 * ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues k / (Matrix.toEuclideanLin (cocycle A T n x)).singularValues (k - 1)) ^ 2) ≤ ∏ i ∈ Finset.range k, lamCocycle A T (n + 1) x i - (∏ i ∈ Finset.range (k - 1), lamCocycle A T n x i) * lamCocycle A T n x k * ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))‖ ^ 2) (hgapμ : (∏ i ∈ Finset.range (k - 1), lamCocycle A T n x i) * lamCocycle A T n x k * ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))‖ ^ 2 < ∏ i ∈ Finset.range k, lamCocycle A T (n + 1) x i) (hκr : (‖ExteriorNorm.compoundMatrix k (A (T^[n] x))‖ * ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))⁻¹‖) ^ 2 * ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues k / (Matrix.toEuclideanLin (cocycle A T n x)).singularValues (k - 1)) ^ 2 < 1) : ‖bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x - bandProjector A T ((Set.Ioi c).indicator 1) n x‖ ≤ √(2 * ↑k) * ((‖ExteriorNorm.compoundMatrix k (A (T^[n] x))‖ * ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))⁻¹‖) ^ 2 * ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues k / (Matrix.toEuclideanLin (cocycle A T n x)).singularValues (k - 1)) / (1 - (‖ExteriorNorm.compoundMatrix k (A (T^[n] x))‖ * ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))⁻¹‖) ^ 2 * ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues k / (Matrix.toEuclideanLin (cocycle A T n x)).singularValues (k - 1)) ^ 2))

The cocycle per-step band-projector increment bound. Instantiating the abstract norm_bandProjector_succ_sub_le with the SORTED Gram eigenframes (bandProjector_indicator_eq_sortedTopFrame), the Plücker eigenpairs of gram n/gram (n+1), and the off-diagonal numerator / ν-ceiling / lower-bound exterior lemmas. With B = A(T^[n] x), cM = ‖compound k Mₙ‖, cB = ‖compound k B‖, cBi = ‖compound k B⁻¹‖, r = σₖ/σₖ₋₁, in the EVENTUAL regime (cB·cBi)²r² < 1, the band projectors satisfy ‖Pₙ₊₁ − Pₙ‖ ≤ √(2k)·(cB·cBi)²·r/(1 − (cB·cBi)²r²). The cut hypotheses (htop*, hcount*) identify both band projectors with the sorted top-k frames; the gap hypotheses (hgap*) feed the Plücker spectral gap; the scalar linkage hypotheses (hμ₀lb, hgapμ, hκr) are the genuine outputs of ExteriorNorm.norm_sq_compound_mul_ge + the eventual regime, discharged a.e. by the unconditional root-test convergence layer below.

A.e. summability of the band-projector increments (the root-test conclusion)

The per-step band-projector bound ‖Pₙ₊₁ − Pₙ‖ ≤ bₙ with bₙ = √(2k)·κ(⋀ᵏB)²·rₙ/(1 − κ²rₙ²) (norm_bandProjector_succ_sub_le) is summable along the orbit by the root test: (1/n)log bₙ → λₖ − λₖ₋₁ < 0. The scalar layer supplies the log-limit ((1/n)log rₙ → λₖ − λₖ₋₁ via tendsto_log_singularValue at indices k, k−1; the κ² factor subexponential via tendsto_logNorm_compound_orbit_div_atTop_zero; the 1/(1−κ²rₙ²) factor → 1 since κ²rₙ² → 0). We package the comparison + root test abstractly, then state the cocycle conclusion taking the per-step bound and the negative log-limit of its RHS as hypotheses (the genuine outputs of the per-step bound norm_bandProjector_succ_sub_le and the scalar layer).

theorem Oseledets.summable_norm_of_logLimit_neg_of_le {E : Type u_2} [NormedAddCommGroup E] (incr : ℕ → E) (b : ℕ → ℝ) (hb : ∀ (n : ℕ), 0 ≤ b n) (hpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < b n) {L : ℝ} (hL : L < 0) (hlog : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (b n)) Filter.atTop (nhds L)) (hstep : ∀ᶠ (n : ℕ) in Filter.atTop, ‖incr n‖ ≤ b n) : Summable fun (n : ℕ) => ‖incr n‖

Packaging: comparison + root test. If the increment norms ‖incr n‖ are eventually dominated by a nonnegative sequence b whose normalized log tends to a negative limit, then the increment norms are summable. Pure soft analysis (summable_of_logLimit_neg + Summable.of_norm_bounded_eventually_nat).

theorem Oseledets.summable_norm_bandProjector_succ_sub {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → X} {c : ℝ} (A : X → Matrix (Fin d) (Fin d) ℝ) (b : X → ℕ → ℝ) (hb : ∀ᵐ (x : X) ∂μ, ∀ (n : ℕ), 0 ≤ b x n) (hpos : ∀ᵐ (x : X) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, 0 < b x n) (L : X → ℝ) (hL : ∀ᵐ (x : X) ∂μ, L x < 0) (hlog : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (b x n)) Filter.atTop (nhds (L x))) (hstep : ∀ᵐ (x : X) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, ‖bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x - bandProjector A T ((Set.Ioi c).indicator 1) n x‖ ≤ b x n) : ∀ᵐ (x : X) ∂μ, Summable fun (n : ℕ) => ‖bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x - bandProjector A T ((Set.Ioi c).indicator 1) n x‖

A.e. summability of the band-projector increments. For μ-a.e. x, the consecutive band-projector increments ‖Pₙ₊₁ − Pₙ‖ are summable. The per-step dominating sequence b x n (the RHS of norm_bandProjector_succ_sub_le, eventually √(2k)·κ²rₙ/(1−κ²rₙ²)), its nonnegativity / eventual positivity, the negative root-test log-limit L x (= λₖ − λₖ₋₁), and the eventual per-step bound are taken as hypotheses — the genuine outputs of the per-step bound and the scalar layer (tendsto_log_singularValue, tendsto_logNorm_compound_orbit_div_atTop_zero). The conclusion is the summability that feeds the Cauchy packaging cauchySeq_cfc_of_summable.

A.e. assembly: the band projectors converge

The Cauchy packaging exists_tendsto_cfc_of_summable turns the a.e. summability of the band-projector increments (summable_norm_bandProjector_succ_sub) into a.e. convergence of the band projectors themselves: the candidate Oseledets spectral projector exists μ-a.e. The bandProjector A T (indicator (Ioi c) 1) n x = cfc (indicator (Ioi c) 1) (qpow A T n x) sequence is the cfc χ (H n) sequence with H = fun n => qpow A T n x, so this is a direct specialization.

theorem Oseledets.exists_tendsto_bandProjector {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → X} {c : ℝ} (A : X → Matrix (Fin d) (Fin d) ℝ) (b : X → ℕ → ℝ) (hb : ∀ᵐ (x : X) ∂μ, ∀ (n : ℕ), 0 ≤ b x n) (hpos : ∀ᵐ (x : X) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, 0 < b x n) (L : X → ℝ) (hL : ∀ᵐ (x : X) ∂μ, L x < 0) (hlog : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (b x n)) Filter.atTop (nhds (L x))) (hstep : ∀ᵐ (x : X) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, ‖bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x - bandProjector A T ((Set.Ioi c).indicator 1) n x‖ ≤ b x n) : ∀ᵐ (x : X) ∂μ, ∃ (P : Matrix (Fin d) (Fin d) ℝ), Filter.Tendsto (fun (n : ℕ) => bandProjector A T ((Set.Ioi c).indicator 1) n x) Filter.atTop (nhds P)

A.e. assembly. For μ-a.e. x, the band projectors bandProjector A T (indicator (Ioi c) 1) n x converge: there is a limiting projector P with Tendsto (fun n => bandProjector A T (indicator (Ioi c) 1) n x) atTop (𝓝 P). This is the convergence of the Oseledets spectral projector pinned by the growing spectral gap, obtained by feeding the a.e. summability of the increments (summable_norm_bandProjector_succ_sub) into the soft-analysis Cauchy packaging exists_tendsto_cfc_of_summable. The summability hypotheses are the genuine outputs of the per-step bound norm_bandProjector_succ_sub_le and the scalar root-test layer (tendsto_log_singularValue, tendsto_logNorm_compound_orbit_div_atTop_zero).

Unconditional band-projector a.e. convergence (cocycle)

Feeding the per-step bound norm_bandProjector_succ_sub_le_cocycle through the Cauchy packaging exists_tendsto_bandProjector: for μ-a.e. x, the band projector bandProjector A T (indicator (Ioi c) 1) n x converges. The per-step bound bCocycle x n = √(2k)·κ²r/(1 − κ²r²) is summable along the orbit by the root test (its (1/n)·log tends to λₖ − λₖ₋₁ < 0 a.e. via the scalar layer tendsto_log_singularValue at the two cut indices and tendsto_logNorm_compound_orbit_div_atTop_zero; the eventual regime κ²r² < 1 holds a.e. since r → 0 geometrically while κ is tempered). The a.e. eventual cut/gap/regime conditions are packaged as stepHypCocycle and discharged through the per-step bound by stepHypCocycle_imp_step.

noncomputable def Oseledets.bCocycle {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (k : ℕ) : ℕ → ℝ

The per-step dominating sequence. The RHS of the cocycle band-projector increment bound (norm_bandProjector_succ_sub_le_cocycle): √(2k)·κ²·r/(1 − κ²r²) with κ = ‖compound k B‖·‖compound k B⁻¹‖, r = σₖ/σₖ₋₁, B = A(T^[n] x). Its (1/n)·log tends to λₖ − λₖ₋₁ < 0 a.e., making it summable by the root test.

Equations

• One or more equations did not get rendered due to their size.

def Oseledets.stepHypCocycle {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (k : ℕ) (hkd : k ≤ Fintype.card (Fin d)) (x : X) (n : ℕ) : Prop

The per-step cut/gap/regime conditions at a single n. The conjunction of all hypotheses of norm_bandProjector_succ_sub_le_cocycle at step n: the cut counts = k (at n and n+1), the top-k sorted qpow eigenvalues exceed c, the Plücker spectral gaps, and the scalar regime/linkage conditions. Eventually true a.e. along the orbit (the cut is stable in the eventual Lyapunov-gap regime; r → 0 geometrically); see the section note above.

Equations

• One or more equations did not get rendered due to their size.

theorem Oseledets.stepHypCocycle_imp_step {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (hA : ∀ (x : X), (A x).det ≠ 0) (c : ℝ) {k : ℕ} (hk1 : 1 ≤ k) (hkd : k ≤ Fintype.card (Fin d)) (x : X) (n : ℕ) (h : stepHypCocycle A T c k hkd x n) : ‖bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x - bandProjector A T ((Set.Ioi c).indicator 1) n x‖ ≤ bCocycle A T x k n

Per-step conditions discharge the increment bound. stepHypCocycle at n gives the band-projector increment bound ‖Pₙ₊₁ − Pₙ‖ ≤ bCocycle x n via norm_bandProjector_succ_sub_le_cocycle.

theorem Oseledets.exists_tendsto_bandProjector_cocycle {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → X} (A : X → Matrix (Fin d) (Fin d) ℝ) (hA : ∀ (x : X), (A x).det ≠ 0) (c : ℝ) {k : ℕ} (hk1 : 1 ≤ k) (hkd : k ≤ Fintype.card (Fin d)) (hstepAE : ∀ᵐ (x : X) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, stepHypCocycle A T c k hkd x n) (hbnn : ∀ᵐ (x : X) ∂μ, ∀ (n : ℕ), 0 ≤ bCocycle A T x k n) (hbpos : ∀ᵐ (x : X) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, 0 < bCocycle A T x k n) (L : X → ℝ) (hLneg : ∀ᵐ (x : X) ∂μ, L x < 0) (hblog : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (bCocycle A T x k n)) Filter.atTop (nhds (L x))) : ∀ᵐ (x : X) ∂μ, ∃ (P : Matrix (Fin d) (Fin d) ℝ), Filter.Tendsto (fun (n : ℕ) => bandProjector A T ((Set.Ioi c).indicator 1) n x) Filter.atTop (nhds P)

Unconditional band-projector a.e. convergence. For μ-a.e. x, the band projector bandProjector A T (indicator (Ioi c) 1) n x converges to a limiting projector P. This is the convergence of the Oseledets spectral projector pinned by the growing spectral gap. The proof discharges the per-step increment bound (via stepHypCocycle_imp_step) from the a.e. eventual cut/gap/regime conditions hstepAE, and feeds the resulting a.e. summability — by the root test on bCocycle (whose (1/n)·log tends to λₖ − λₖ₋₁ < 0 a.e., supplied as hblog/hLneg by the scalar layer) — into the soft-analysis Cauchy packaging exists_tendsto_bandProjector. The hypotheses hstepAE, hblog, hLneg, hbnn, hbpos are the genuine outputs of the ergodic Lyapunov-spectrum structure and the scalar root-test layer (tendsto_log_singularValue, tendsto_logNorm_compound_orbit_div_atTop_zero); the conclusion is the UNCONDITIONAL a.e. existence of the limiting Oseledets band projector.

theorem Oseledets.tendsto_zero_of_logLimit_neg (a : ℕ → ℝ) (hnn : ∀ (n : ℕ), 0 ≤ a n) (hpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < a n) {L : ℝ} (hL : L < 0) (hlog : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (a n)) Filter.atTop (nhds L)) : Filter.Tendsto a Filter.atTop (nhds 0)

A nonnegative, eventually-positive sequence whose normalized log tends to a negative limit converges to 0. (Root test ⟹ summable ⟹ tail vanishes.)

theorem Oseledets.tendsto_log_bCocycle_point {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) {x : X} {k : ℕ} (hk1 : 1 ≤ k) (hkd : k < d) {lamK lamK1 : ℝ} (hσk : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues k)) Filter.atTop (nhds lamK)) (hσk1 : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues (k - 1))) Filter.atTop (nhds lamK1)) (hcomp : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))‖) Filter.atTop (nhds 0)) (hcompinv : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))⁻¹‖) Filter.atTop (nhds 0)) (hgap : lamK < lamK1) : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (bCocycle A T x k n)) Filter.atTop (nhds (lamK - lamK1))

Per-point log-limit for bCocycle.

theorem Oseledets.card_eigenvalues_gt_eq_card_eigenvalues₀_gt {d : ℕ} [NeZero d] {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.IsHermitian) (c : ℝ) : Fintype.card { i : Fin d // c < hM.eigenvalues i } = Fintype.card { j : Fin (Fintype.card (Fin d)) // c < hM.eigenvalues₀ j }

The count of unsorted eigenvalues > c equals the count of sorted eigenvalues > c.

theorem Oseledets.card_antitone_gt_eq {N : ℕ} (f : Fin N → ℝ) (hf : Antitone f) (c : ℝ) {k : ℕ} (hk1 : 1 ≤ k) (hkN : k < N) (htop : c < f ⟨k - 1, ⋯⟩) (hbot : f ⟨k, hkN⟩ < c) : Fintype.card { j : Fin N // c < f j } = k

If an antitone Fin N → ℝ family has its value at index ⟨k-1⟩ above c and at index ⟨k⟩ below c, then exactly k of its values exceed c.

theorem Oseledets.step_inequalities {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (n : ℕ) (x : X) {k : ℕ} (hk1 : 1 ≤ k) (hkd : k < d) (hcBipos : 0 < ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))⁻¹‖) (hκr : (‖ExteriorNorm.compoundMatrix k (A (T^[n] x))‖ * ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))⁻¹‖) ^ 2 * ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues k / (Matrix.toEuclideanLin (cocycle A T n x)).singularValues (k - 1)) ^ 2 < 1) : ‖ExteriorNorm.compoundMatrix k (cocycle A T n x)‖ ^ 2 / ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))⁻¹‖ ^ 2 * (1 - (‖ExteriorNorm.compoundMatrix k (A (T^[n] x))‖ * ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))⁻¹‖) ^ 2 * ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues k / (Matrix.toEuclideanLin (cocycle A T n x)).singularValues (k - 1)) ^ 2) ≤ ∏ i ∈ Finset.range k, lamCocycle A T (n + 1) x i - (∏ i ∈ Finset.range (k - 1), lamCocycle A T n x i) * lamCocycle A T n x k * ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))‖ ^ 2 ∧ (∏ i ∈ Finset.range (k - 1), lamCocycle A T n x i) * lamCocycle A T n x k * ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))‖ ^ 2 < ∏ i ∈ Finset.range k, lamCocycle A T (n + 1) x i

The two scalar inequalities hμ₀lb/hgapμ of stepHypCocycle, from the compound lower bound μ̃₀ ≥ cM²/cBi² (norm_sq_compound_mul_ge) and the regime κ²r² < 1.

theorem Oseledets.bCocycle_pos_of_regime {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (x : X) {k : ℕ} (hk1 : 1 ≤ k) (hkd : k < d) (n : ℕ) (hκr : (‖ExteriorNorm.compoundMatrix k (A (T^[n] x))‖ * ‖ExteriorNorm.compoundMatrix k (A (T^[n] x))⁻¹‖) ^ 2 * ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues k / (Matrix.toEuclideanLin (cocycle A T n x)).singularValues (k - 1)) ^ 2 < 1) : 0 < bCocycle A T x k n

bCocycle is positive once the regime κ²r² < 1 holds.

theorem Oseledets.tendsto_bandProjector_of_gap {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) (c : ℝ) {k : ℕ} (hk1 : 1 ≤ k) (hkd : k < d) (lamK lamK1 : ℝ) (hgap : lamK < lamK1) (hclo : Real.exp lamK < c) (hchi : c < Real.exp lamK1) (hσkAE : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues k)) Filter.atTop (nhds lamK)) (hσk1AE : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues (k - 1))) Filter.atTop (nhds lamK1)) : ∀ᵐ (x : X) ∂μ, ∃ (P : Matrix (Fin d) (Fin d) ℝ), Filter.Tendsto (fun (n : ℕ) => bandProjector A T ((Set.Ioi c).indicator 1) n x) Filter.atTop (nhds P)

Unconditional band-projector a.e. convergence at a distinct-exponent gap. For an ergodic, integrable, invertible cocycle and a threshold c strictly between the exponentials of two consecutive distinct Lyapunov exponents at the cut index k (e^{λₖ} < c < e^{λₖ₋₁} with λₖ < λₖ₋₁), the band spectral projector converges μ-a.e.