Weyl eigenvalue-perturbation for symmetric operators / Hermitian matrices

The sorted eigenvalues of a self-adjoint operator are 1-Lipschitz in the operator norm of the difference (the Weyl perturbation inequality, a consequence of the Courant–Fischer min-max characterization). Mathlib's Mathlib/Analysis/InnerProductSpace/Rayleigh.lean provides only the extreme eigenvalues as Rayleigh iSup/iInf; the per-index variational bound here — and the resulting continuity of Matrix.IsHermitian.eigenvalues₀ — are new, and are the analytic ingredient that lets the eigenvalues pass to the Oseledets matrix limit.

Main results

• Oseledets.Weyl.abs_eigenvalues₀_sub_le — the Weyl perturbation inequality: sorted eigenvalues of Hermitian matrices are 1-Lipschitz in the L² operator norm.
• Oseledets.Weyl.tendsto_eigenvalues₀ — continuity of the sorted eigenvalues along limits.

theorem Oseledets.Weyl.quad_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →ₗ[ℝ] E} (hT : T.IsSymmetric) (hn : Module.finrank ℝ E = n) (v : E) : inner ℝ (T v) v = ∑ i : Fin n, hT.eigenvalues hn i * inner ℝ ((hT.eigenvectorBasis hn) i) v ^ 2

Expansion of the quadratic form ⟪T v, v⟫ of a symmetric operator in its orthonormal eigenbasis: ⟪T v, v⟫ = ∑ᵢ μᵢ ⟪bᵢ, v⟫² where μ are the sorted eigenvalues and b the eigenvector basis.

theorem Oseledets.Weyl.normsq_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →ₗ[ℝ] E} (hT : T.IsSymmetric) (hn : Module.finrank ℝ E = n) (v : E) : ‖v‖ ^ 2 = ∑ i : Fin n, inner ℝ ((hT.eigenvectorBasis hn) i) v ^ 2

Expansion of ‖v‖² in an orthonormal eigenbasis: ‖v‖² = ∑ᵢ ⟪bᵢ, v⟫².

def Oseledets.Weyl.spanP {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →ₗ[ℝ] E} (hT : T.IsSymmetric) (hn : Module.finrank ℝ E = n) (p : Fin n → Prop) [DecidablePred p] : Submodule ℝ E

The subspace spanned by the eigenvectors whose (sorted) index satisfies the predicate p.

Equations

• Oseledets.Weyl.spanP hT hn p = Submodule.span ℝ (⇑(hT.eigenvectorBasis hn).toBasis '' {j : Fin n | p j})

theorem Oseledets.Weyl.mem_spanP {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →ₗ[ℝ] E} (hT : T.IsSymmetric) (hn : Module.finrank ℝ E = n) {p : Fin n → Prop} [DecidablePred p] {v : E} : v ∈ spanP hT hn p ↔ ∀ (j : Fin n), ¬p j → inner ℝ ((hT.eigenvectorBasis hn) j) v = 0

Membership in spanP p: the inner products against the off-p eigenvectors vanish.

theorem Oseledets.Weyl.finrank_spanP {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →ₗ[ℝ] E} (hT : T.IsSymmetric) (hn : Module.finrank ℝ E = n) (p : Fin n → Prop) [DecidablePred p] : Module.finrank ℝ ↥(spanP hT hn p) = (Finset.filter p Finset.univ).card

The dimension of spanP p equals the number of sorted indices satisfying p.

theorem Oseledets.Weyl.quad_ge_on_top {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →ₗ[ℝ] E} (hT : T.IsSymmetric) (hn : Module.finrank ℝ E = n) (i : Fin n) {v : E} (hv : v ∈ spanP hT hn fun (x : Fin n) => x ≤ i) : hT.eigenvalues hn i * ‖v‖ ^ 2 ≤ inner ℝ (T v) v

On the span of the top i + 1 eigenvectors, the quadratic form is at least μᵢ ‖v‖² (the i-th eigenvalue is the smallest of the top i + 1).

theorem Oseledets.Weyl.quad_le_on_bot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →ₗ[ℝ] E} (hT : T.IsSymmetric) (hn : Module.finrank ℝ E = n) (i : Fin n) {v : E} (hv : v ∈ spanP hT hn fun (x : Fin n) => i ≤ x) : inner ℝ (T v) v ≤ hT.eigenvalues hn i * ‖v‖ ^ 2

On the span of the bottom n - i eigenvectors, the quadratic form is at most μᵢ ‖v‖² (the i-th eigenvalue is the largest of the bottom n - i).

theorem Oseledets.Weyl.eigenvalues_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →ₗ[ℝ] E} (hT : T.IsSymmetric) (hn : Module.finrank ℝ E = n) {S : E →ₗ[ℝ] E} (hS : S.IsSymmetric) {C : ℝ} (hC : ∀ (v : E), inner ℝ ((T - S) v) v ≤ C * ‖v‖ ^ 2) (i : Fin n) : hT.eigenvalues hn i - hS.eigenvalues hn i ≤ C

Weyl one-sided inequality. If ⟪(T - S) v, v⟫ ≤ C ‖v‖² for all v, then the i-th sorted eigenvalue of T exceeds that of S by at most C. The proof is the Courant–Fischer dimension count: the top-(i+1) eigenspace of T (dim i+1) and the bottom-(n-i) eigenspace of S (dim n-i) sum to dimension n+1 > n, hence meet in a nonzero vector.

theorem Oseledets.Weyl.abs_eigenvalues_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →ₗ[ℝ] E} (hT : T.IsSymmetric) (hn : Module.finrank ℝ E = n) {S : E →ₗ[ℝ] E} (hS : S.IsSymmetric) {C : ℝ} (hC : ∀ (v : E), |inner ℝ ((T - S) v) v| ≤ C * ‖v‖ ^ 2) (i : Fin n) : |hT.eigenvalues hn i - hS.eigenvalues hn i| ≤ C

Weyl perturbation (two-sided). If |⟪(T - S) v, v⟫| ≤ C ‖v‖² for all v, then the i-th sorted eigenvalues of T and S differ by at most C.

theorem Oseledets.Weyl.matrix_quad_le_opNorm {d : ℕ} (A B : Matrix (Fin d) (Fin d) ℝ) (v : EuclideanSpace ℝ (Fin d)) : |inner ℝ ((Matrix.toEuclideanLin A - Matrix.toEuclideanLin B) v) v| ≤ ‖A - B‖ * ‖v‖ ^ 2

The quadratic-form / operator-norm bound for a matrix difference in EuclideanSpace: |⟪(A - B) v, v⟫| ≤ ‖A - B‖ ‖v‖² (with ‖·‖ the L² operator norm).

theorem Oseledets.Weyl.abs_eigenvalues₀_sub_le {d : ℕ} {A B : Matrix (Fin d) (Fin d) ℝ} (hA : A.IsHermitian) (hB : B.IsHermitian) (i : Fin (Fintype.card (Fin d))) : |hA.eigenvalues₀ i - hB.eigenvalues₀ i| ≤ ‖A - B‖

Weyl eigenvalue perturbation for Hermitian matrices. The sorted eigenvalues eigenvalues₀ of real symmetric (Hermitian) d × d matrices are 1-Lipschitz in the L² operator norm of the difference: |eigenvalues₀ A i − eigenvalues₀ B i| ≤ ‖A − B‖.

theorem Oseledets.Weyl.tendsto_eigenvalues₀ {d : ℕ} {ι : Type u_1} {l : Filter ι} {M : ι → Matrix (Fin d) (Fin d) ℝ} {M₀ : Matrix (Fin d) (Fin d) ℝ} (hM : ∀ (k : ι), (M k).IsHermitian) (hM₀ : M₀.IsHermitian) (hconv : Filter.Tendsto M l (nhds M₀)) (i : Fin (Fintype.card (Fin d))) : Filter.Tendsto (fun (k : ι) => ⋯.eigenvalues₀ i) l (nhds (hM₀.eigenvalues₀ i))

Continuity of the sorted eigenvalues. If M_· converges to M₀ (in the matrix topology) and every term and the limit are Hermitian, then the i-th sorted eigenvalue converges.