Forward spectral-rank / dimension formula (two-sided MET)

This module records the forward dimension formula for the slow spectral filtration vslow of the sanitized Oseledets limit operator: almost everywhere,

finrank (vslow A T (exp t) x) = #{j < d | lam0 j ≤ t}.

Main results

• cfc_apply_of_eigenvector — per-point continuous functional calculus on an eigenvector: for a self-adjoint matrix M with toEuclideanLin M v = c • v, one has toEuclideanLin (cfc f M) v = f c • v. No measurability content.
• finrank_range_of_orthonormal_diag — the rank of a self-adjoint idempotent matrix that is diagonal in an orthonormal basis with 0/1 eigenvalues equals the number of unit eigenvalues.
• ae_finrank_vslow — the validated a.e. dimension formula for vslow.

The eigenvector CFC lemma generalises the repo's toEuclideanLin_cfc_fix_eigenvector (which only handles the unit-eigenvalue case); the rank lemma mirrors the eigenbasis-span counting argument of ExteriorNorm.finrank_spanP.

Per-point CFC on an eigenvector

theorem Oseledets.cfc_apply_of_eigenvector {d : ℕ} [NeZero d] (M : Matrix (Fin d) (Fin d) ℝ) (hM : M.IsHermitian) (f : ℝ → ℝ) (v : EuclideanSpace ℝ (Fin d)) {c : ℝ} (hev : (Matrix.toEuclideanLin M) v = c • v) : (Matrix.toEuclideanLin (cfc f M)) v = f c • v

CFC acts as f c on an eigenvector. If M is Hermitian and v is an eigenvector of toEuclideanLin M with eigenvalue c, then toEuclideanLin (cfc f M) v = f c • v.

Proof: expand v in the orthonormal eigenvector basis of M; the component ⟪b_j, v⟫ is nonzero only for indices with eigenvalues j = c (eigenvectors at distinct eigenvalues are orthogonal because M is self-adjoint), and the CFC acts diagonally there as f (eigenvalues j) = f c. This is pointwise, so it carries no measurability content.

Rank of a diagonalised projection

theorem Oseledets.finrank_range_of_orthonormal_diag {d : ℕ} (b : OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d))) (Q : Matrix (Fin d) (Fin d) ℝ) (hidem : Q * Q = Q) (ε : Fin d → ℝ) (hdiag : ∀ (e : Fin d), (Matrix.toEuclideanLin Q) (b e) = ε e • b e) (h01 : ∀ (e : Fin d), ε e = 0 ∨ ε e = 1) : Module.finrank ℝ ↥(↑(Matrix.toEuclideanCLM Q)).range = {e : Fin d | ε e = 1}.card

Rank of a self-adjoint idempotent that is diagonal in an orthonormal basis. If a matrix Q is idempotent (Q * Q = Q) and acts diagonally on an orthonormal basis b with eigenvalues ε e ∈ {0, 1}, then the rank of its range equals the number of unit eigenvalues.

Proof: membership in range (toEuclideanCLM Q) is toEuclideanLin Q v = v, which — expanded in the basis — is exactly the vanishing of all components against the zero-eigenvalue vectors. This is the same membership predicate as the span of the unit-eigenvalue vectors, so the range equals that span, whose dimension is the cardinality of the unit-eigenvalue set (orthonormal vectors are linearly independent).

The a.e. dimension formula for vslow

theorem Oseledets.ae_finrank_vslow {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X → X} {d : ℕ} [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 : ℝ), Module.finrank ℝ ↥(vslow A T (Real.exp t) x) = {j ∈ Finset.range d | lam0 j ≤ t}.card

A.e. forward dimension formula. Almost everywhere, the dimension of the slow spectral filtration vslow A T (exp t) x at threshold t is the number of indices j < d whose deterministic exponent lam0 j does not exceed t.