Limit eigenbasis of the Oseledets limit operator

This module builds the limit eigenbasis of the sanitized (everywhere self-adjoint) Oseledets limit operator lambdaHat A T x, indexed by Fin d and sorted decreasingly consistently with Matrix.IsHermitian.eigenvalues₀.

Main results

• limitEigenbasis — the sorted orthonormal eigenbasis of lambdaHat A T x.
• limitEigenbasis_eigenpair — the everywhere eigenpair identity, with eigenvalue eigenvalues₀ ⟨e, …⟩.
• limitEigenbasis_eigenpair_exp — a.e. the eigenvalue is Real.exp (lamSing A T x e).
• inner_limitEigenbasis_eq_zero_of_slow — a.e., a sorted eigenvector is orthogonal to the slow subspace vslow A T (exp t) x whenever its exponent strictly exceeds t.
• abs_inner_le_one_bases — the trivial Cauchy–Schwarz bound for orthonormal bases.

The sorted limit eigenbasis

noncomputable def Oseledets.limitEigenbasis {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) : OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d))

The sorted limit eigenbasis. The orthonormal eigenbasis of the everywhere self-adjoint sanitized limit lambdaHat A T x, reindexed by Fin d so that limitEigenbasis A T x e has eigenvalue eigenvalues₀ ⟨e, …⟩ (antitone, descending). Built by mimicking sortedGramEigenbasis: take the eigenvector basis of (lambdaHat_isSelfAdjoint A T x).isHermitian, reindex from Fin d to Fin (card (Fin d)) (the sorted index), then finCongr back to Fin d.

Equations

• Oseledets.limitEigenbasis A T x = (⋯.eigenvectorBasis.reindex (Fintype.equivOfCardEq ⋯).symm).reindex (finCongr ⋯)

The everywhere eigenpair

theorem Oseledets.limitEigenbasis_eigenpair {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (e : Fin d) : (Matrix.toEuclideanLin (lambdaHat A T x)) ((limitEigenbasis A T x) e) = ⋯.eigenvalues₀ ⟨↑e, ⋯⟩ • (limitEigenbasis A T x) e

The everywhere eigenpair. limitEigenbasis A T x e is an eigenvector of toEuclideanLin (lambdaHat A T x) with eigenvalue the sorted eigenvalue eigenvalues₀ ⟨e, …⟩. Mimics sortedGramEigenbasis_eigenpair.

Almost-everywhere eigenvalue identification as exp (lamSing)

theorem Oseledets.limitEigenbasis_eigenpair_exp {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {d : ℕ} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] [NeZero d] (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)⁻¹) μ) : ∀ᵐ (x : X) ∂μ, ∀ (e : Fin d), (Matrix.toEuclideanLin (lambdaHat A T x)) ((limitEigenbasis A T x) e) = Real.exp (lamSing A T x ↑e) • (limitEigenbasis A T x) e

A.e. eigenvalue identification. On the a.e. set where the Oseledets limit is Hermitian, lambdaHat = oseledetsLimit, and the sorted eigenvalue equals Real.exp (lamSing A T x e).

The Cauchy–Schwarz bound for orthonormal bases

theorem Oseledets.abs_inner_le_one_bases {d : ℕ} (b₁ b₂ : OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d))) (i j : Fin d) : |inner ℝ (b₁ i) (b₂ j)| ≤ 1

The trivial inner-product bound between two orthonormal bases. |⟪b₁ i, b₂ j⟫| ≤ 1 by Cauchy–Schwarz and the unit norms of orthonormal-basis vectors.

Orthogonality to the slow subspace

theorem Oseledets.inner_limitEigenbasis_eq_zero_of_slow {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {d : ℕ} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] [NeZero d] (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)⁻¹) μ) (lam0 : ℕ → ℝ) (hlam0 : ∀ i < d, ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues i)) Filter.atTop (nhds (lam0 i))) : ∀ᵐ (x : X) ∂μ, ∀ (t : ℝ), ∀ v ∈ vslow A T (Real.exp t) x, ∀ (e : Fin d), t < lam0 ↑e → inner ℝ ((limitEigenbasis A T x) e) v = 0

Slow orthogonality. A.e., a sorted limit eigenvector limitEigenbasis A T x e whose exponent lam0 e strictly exceeds the cutoff t is orthogonal to every vector in the slow subspace vslow A T (exp t) x.

Route: v ∈ vslow means slowProjector fixes v; self-adjointness moves the projector onto the eigenvector, where the indicator-CFC slowProjector annihilates it (its eigenvalue exp (lam0 e) exceeds exp t, outside Iic (exp t)).