Band-projector limit identification and the reverse slow-flag inclusion

Main results:

1. tendsto_cfc_of_tendsto_of_lipschitz — the continuous functional calculus of a (Lipschitz, hence continuous) function is continuous under matrix limits of Hermitian matrices.
2. ae_tendsto_bandProjector_cfc_indicator — a.e., the band projector limit at a non-eigenvalue threshold c is the Λ-spectral projector cfc 𝟙_{(c,∞)} (lambdaHat …).
3. ae_lambdaSublevel_le_vslow — the reverse slow-flag inclusion lambdaSublevel t ⊆ vslow (e^t).

The first result rests on a Frobenius / Hilbert–Schmidt Lipschitz estimate for the functional calculus; the second uses a continuous Lipschitz clamp surrogate for the indicator of (c, ∞) to transfer convergence through the calculus; the third combines the spectral identification with the Furstenberg–Kesten growth bounds to obtain the inclusion of sublevel sets into slow spaces.

The functional calculus is matrix-limit continuous for Lipschitz functions

We prove the Frobenius / Hilbert–Schmidt Lipschitz bound: for Hermitian A, B and K-Lipschitz f, HS_B (cfc f A - cfc f B) ≤ K² HS_B (A - B), where HS_B Y := ∑ⱼ ‖toEuclideanLin Y (vⱼ)‖² and {vⱼ} is the eigenbasis of B. The per-j bound holds because vⱼ is an eigenvector of B: expanding in the eigenbasis {uᵢ} of A, ⟪uᵢ, (cfc f A − cfc f B) vⱼ⟫ = (f αᵢ − f βⱼ)⟪uᵢ, vⱼ⟫ and ⟪uᵢ, (A − B) vⱼ⟫ = (αᵢ − βⱼ)⟪uᵢ, vⱼ⟫, so |f αᵢ − f βⱼ| ≤ K |αᵢ − βⱼ| gives it termwise. The convergence then follows by an injective-linear-map (antilipschitz) sandwich.

theorem Oseledets.norm_sq_toEuclideanLin_cfc_sub_eigenvectorBasis_le {d : ℕ} [NeZero d] {A B : Matrix (Fin d) (Fin d) ℝ} (hA : A.IsHermitian) (hB : B.IsHermitian) {f : ℝ → ℝ} {K : NNReal} (hf : LipschitzWith K f) (j : Fin d) : ‖(Matrix.toEuclideanLin (cfc f A - cfc f B)) (hB.eigenvectorBasis j)‖ ^ 2 ≤ ↑K ^ 2 * ‖(Matrix.toEuclideanLin (A - B)) (hB.eigenvectorBasis j)‖ ^ 2

Per-eigenvector Frobenius bound: with vⱼ an eigenvector of B, the cfc-difference applied to vⱼ is controlled (squared norm) by K² times the matrix-difference applied to vⱼ.

theorem Oseledets.tendsto_cfc_of_tendsto_of_lipschitz {d : ℕ} [NeZero d] {M : ℕ → Matrix (Fin d) (Fin d) ℝ} {L : Matrix (Fin d) (Fin d) ℝ} (hM : ∀ (n : ℕ), (M n).IsHermitian) (hL : L.IsHermitian) {f : ℝ → ℝ} {K : NNReal} (hf : LipschitzWith K f) (hlim : Filter.Tendsto M Filter.atTop (nhds L)) : Filter.Tendsto (fun (n : ℕ) => cfc f (M n)) Filter.atTop (nhds (cfc f L))

The continuous functional calculus of a Lipschitz (hence continuous) function is continuous under matrix limits of Hermitian matrices: if M n → L with all M n and L Hermitian, then cfc f (M n) → cfc f L.

The band-projector limit is the Λ-spectral projector

noncomputable def Oseledets.clampSurrogate (c h : ℝ) : ℝ → ℝ

A continuous clamp surrogate χ for the indicator of (c, ∞): χ = 0 on (-∞, c], χ = 1 on [c + h, ∞), linear in between, Lipschitz with constant h⁻¹ for h > 0.

Equations

• Oseledets.clampSurrogate c h t = max 0 (min 1 ((t - c) / h))

theorem Oseledets.clampSurrogate_continuous (c h : ℝ) : Continuous (clampSurrogate c h)

theorem Oseledets.clampSurrogate_lipschitz {c h : ℝ} (hh : 0 < h) : ∃ (K : NNReal), LipschitzWith K (clampSurrogate c h)

theorem Oseledets.clampSurrogate_eq_zero {c h : ℝ} (hh : 0 < h) {t : ℝ} (ht : t ≤ c) : clampSurrogate c h t = 0

clampSurrogate c h t = 0 for t ≤ c.

theorem Oseledets.clampSurrogate_eq_one {c h : ℝ} (hh : 0 < h) {t : ℝ} (ht : c + h ≤ t) : clampSurrogate c h t = 1

clampSurrogate c h t = 1 for t ≥ c + h.

theorem Oseledets.exists_eigenvalues₀_eq_of_mem_spectrum {d : ℕ} {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.IsHermitian) {s : ℝ} (hs : s ∈ spectrum ℝ M) : ∃ (i : Fin (Fintype.card (Fin d))), hM.eigenvalues₀ i = s

Every real spectrum value of a Hermitian matrix is one of its sorted eigenvalues eigenvalues₀.

theorem Oseledets.ae_tendsto_bandProjector_cfc_indicator {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X → X} (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) ∂μ, ∀ (c : ℝ), 0 < c → (∀ (i : Fin d), Real.exp (lamSing A T x ↑i) ≠ c) → Filter.Tendsto (fun (n : ℕ) => bandProjector A T ((Set.Ioi c).indicator 1) n x) Filter.atTop (nhds (cfc ((Set.Ioi c).indicator 1) (lambdaHat A T x)))

A.e., for every threshold c > 0 that is not one of the limiting eigenvalues e^{lamSing i}, the band projector cfc 𝟙_{(c,∞)} (qpow n) converges to the Λ-spectral projector cfc 𝟙_{(c,∞)} (lambdaHat A T x).

The reverse slow-flag inclusion

theorem Oseledets.ae_lambdaSublevel_le_vslow {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X → X} (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) ∂μ, ∀ (t : ℝ), lambdaSublevel A T x t ≤ vslow A T (Real.exp t) x

A.e., for every t, the lambdaBar-sublevel at t is contained in the Λ-slow space vslow (e^t). This is the inclusion consumed by Oseledets.oseledets_filtration_of_upper.