Spectral lemmas for a real symmetric matrix

Generic facts behind Theorem 33 of the Survey (Lovász 1993, Theorem 5.1), for a real symmetric matrix A with Mathlib's orthonormal eigenbasis bₖ = hA.eigenvectorBasis k and eigenvalues μₖ = hA.eigenvalues k, written with plain dot products:

• completeness ∑ₖ bₖ(u) bₖ(v) = δᵤᵥ, orthonormality, and Parseval y ⬝ z = ∑ₖ (bₖ ⬝ y)(bₖ ⬝ z);
• bₖ ⬝ (A z) = μₖ (bₖ ⬝ z);
• |μₖ| ≤ 1 when the quadratic form satisfies |w ⬝ A w| ≤ w ⬝ w;
• contraction on the complement of a unit eigenvector s for the eigenvalue 1: if all eigenvalues satisfy |μ| ≤ 1 and at most one satisfies |μ| > λ, then ‖A y‖ ≤ λ ‖y‖ for y ⊥ s;
• the entry bound |Aᵗ(u, v) - s(u) s(v)| ≤ λᵗ.

theorem Averaging.sum_eigenvectorBasis_mul_eigenvectorBasis {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (u v : V) : ∑ k : V, (hA.eigenvectorBasis k).ofLp u * (hA.eigenvectorBasis k).ofLp v = if u = v then 1 else 0

Completeness of the eigenbasis: ∑ₖ bₖ(u) bₖ(v) = δᵤᵥ.

theorem Averaging.eigenvectorBasis_dotProduct {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (k l : V) : (hA.eigenvectorBasis k).ofLp ⬝ᵥ (hA.eigenvectorBasis l).ofLp = if k = l then 1 else 0

Orthonormality of the eigenbasis: bₖ ⬝ bₗ = δₖₗ.

theorem Averaging.dotProduct_eq_sum_eigenvectorBasis {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (y z : V → ℝ) : y ⬝ᵥ z = ∑ k : V, (hA.eigenvectorBasis k).ofLp ⬝ᵥ y * (hA.eigenvectorBasis k).ofLp ⬝ᵥ z

Parseval: y ⬝ z = ∑ₖ (bₖ ⬝ y)(bₖ ⬝ z).

theorem Averaging.eigenvectorBasis_dotProduct_mulVec {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (k : V) (z : V → ℝ) : (hA.eigenvectorBasis k).ofLp ⬝ᵥ A.mulVec z = hA.eigenvalues k * (hA.eigenvectorBasis k).ofLp ⬝ᵥ z

The coefficients of A z: bₖ ⬝ (A z) = μₖ (bₖ ⬝ z).

theorem Averaging.dotProduct_mulVec_comm {V : Type u_1} [Fintype V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (y z : V → ℝ) : y ⬝ᵥ A.mulVec z = A.mulVec y ⬝ᵥ z

A symmetric matrix moves between the two sides of a dot product.

theorem Averaging.abs_eigenvalues_le_one {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (hq : ∀ (w : V → ℝ), |w ⬝ᵥ A.mulVec w| ≤ w ⬝ᵥ w) (k : V) : |hA.eigenvalues k| ≤ 1

If the quadratic form satisfies |w ⬝ A w| ≤ w ⬝ w, every eigenvalue has |μ| ≤ 1.

theorem Averaging.mulVec_dotProduct_mulVec_le {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (s : V → ℝ) (hs : A.mulVec s = s) (hs1 : s ⬝ᵥ s = 1) {lam : ℝ} (hle : ∀ (k : V), |hA.eigenvalues k| ≤ 1) (huniq : ∀ (k l : V), lam < |hA.eigenvalues k| → lam < |hA.eigenvalues l| → k = l) (y : V → ℝ) (hy : s ⬝ᵥ y = 0) : A.mulVec y ⬝ᵥ A.mulVec y ≤ lam ^ 2 * y ⬝ᵥ y

Contraction on the complement of s: if s is a unit eigenvector for the eigenvalue 1, every eigenvalue has |μ| ≤ 1 and at most one has |μ| > λ, then ‖A y‖² ≤ λ² ‖y‖² for every y ⊥ s.

theorem Averaging.pow_mulVec_of_mulVec_eq {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (s : V → ℝ) (hs : A.mulVec s = s) (t : ℕ) : (A ^ t).mulVec s = s

The powers of A fix s and keep the complement of s.

theorem Averaging.pow_mulVec_dotProduct_le {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (s : V → ℝ) (hs : A.mulVec s = s) {lam : ℝ} (hcontr : ∀ (y : V → ℝ), s ⬝ᵥ y = 0 → A.mulVec y ⬝ᵥ A.mulVec y ≤ lam ^ 2 * y ⬝ᵥ y) (y : V → ℝ) (hy : s ⬝ᵥ y = 0) (t : ℕ) : s ⬝ᵥ (A ^ t).mulVec y = 0 ∧ (A ^ t).mulVec y ⬝ᵥ (A ^ t).mulVec y ≤ lam ^ (2 * t) * y ⬝ᵥ y

Contraction by λᵗ of Aᵗ on the complement of s.

theorem Averaging.abs_pow_apply_sub_le {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (s : V → ℝ) (hs : A.mulVec s = s) (hs1 : s ⬝ᵥ s = 1) {lam : ℝ} (hlam : 0 ≤ lam) (hcontr : ∀ (y : V → ℝ), s ⬝ᵥ y = 0 → A.mulVec y ⬝ᵥ A.mulVec y ≤ lam ^ 2 * y ⬝ᵥ y) (t : ℕ) (u v : V) : |(A ^ t) u v - s u * s v| ≤ lam ^ t

The entry bound |Aᵗ(u, v) - s(u) s(v)| ≤ λᵗ, from the contraction on the complement of a unit eigenvector s for the eigenvalue 1.