Spectral facts for real symmetric matrices, on plain vectors

For a real symmetric matrix A on V, Mathlib's orthonormal eigenbasis Matrix.IsHermitian.eigenvectorBasis lives in EuclideanSpace ℝ V. Here its vectors are read as plain functions V → ℝ with the dot product ⬝ᵥ: orthonormality, the expansion of a vector in the basis, Parseval's identity, and the contraction bound ‖Aᵗ y‖² ≤ λ²ᵗ ‖y‖² for vectors y without components along eigenvectors whose eigenvalue exceeds λ in absolute value. These are the linear-algebra inputs of Lemma C.1 of Becchetti et al. (arXiv:1511.03927).

noncomputable def Averaging.eigvec {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (j : V) : V → ℝ

The j-th vector of the orthonormal eigenbasis of A, as a plain function.

Equations

• Averaging.eigvec hA j = (hA.eigenvectorBasis j).ofLp

theorem Averaging.eigvec_dotProduct_eigvec {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (i j : V) : eigvec hA i ⬝ᵥ eigvec hA j = if i = j then 1 else 0

theorem Averaging.mulVec_eigvec {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (j : V) : A.mulVec (eigvec hA j) = hA.eigenvalues j • eigvec hA j

theorem Averaging.sum_dotProduct_smul_eigvec {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (u : V → ℝ) : ∑ j : V, (eigvec hA j ⬝ᵥ u) • eigvec hA j = u

Expansion of a vector in the orthonormal eigenbasis.

theorem Averaging.sum_dotProduct_mul_dotProduct {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (u v : V → ℝ) : ∑ j : V, eigvec hA j ⬝ᵥ u * eigvec hA j ⬝ᵥ v = u ⬝ᵥ v

Parseval's identity in the eigenbasis.

theorem Averaging.pow_mulVec_eigvec {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (t : ℕ) (j : V) : (A ^ t).mulVec (eigvec hA j) = hA.eigenvalues j ^ t • eigvec hA j

theorem Averaging.eigvec_dotProduct_pow_mulVec {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) (t : ℕ) (j : V) (y : V → ℝ) : eigvec hA j ⬝ᵥ (A ^ t).mulVec y = hA.eigenvalues j ^ t * eigvec hA j ⬝ᵥ y

The coefficient of Aᵗ y along an eigenvector is νᵗ times that of y (symmetry of A).

theorem Averaging.pow_mulVec_dotProduct_self_le {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) {lam : ℝ} {y : V → ℝ} (hy : ∀ (j : V), lam < |hA.eigenvalues j| → eigvec hA j ⬝ᵥ y = 0) (t : ℕ) : (A ^ t).mulVec y ⬝ᵥ (A ^ t).mulVec y ≤ (lam ^ t) ^ 2 * y ⬝ᵥ y

Contraction: if y has no component along eigenvectors with |ν| > λ, then ‖Aᵗ y‖² ≤ λ²ᵗ ‖y‖².

theorem Averaging.card_filter_lt_abs_eigenvalues_le_two {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) {lam : ℝ} (hlam : ∀ (i : Fin (Fintype.card V)), 2 ≤ ↑i → |hA.eigenvalues₀ i| ≤ lam) : {j : V | lam < |hA.eigenvalues j|}.card ≤ 2

At most two eigenvalues exceed in absolute value a bound on all but the two largest ones of the decreasingly sorted spectrum eigenvalues₀.

theorem Averaging.eigvec_dotProduct_eq_zero_of_mulVec_eq_smul {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) {u : V → ℝ} {c : ℝ} (hu : A.mulVec u = c • u) {j : V} (hj : hA.eigenvalues j ≠ c) : eigvec hA j ⬝ᵥ u = 0

Eigenvectors for distinct eigenvalues of a symmetric matrix are orthogonal.

Projection on the span of two orthogonal vectors of equal norm

theorem Averaging.residual_dotProduct_left {V : Type u_1} [Fintype V] {u₁ u₂ : V → ℝ} {m : ℝ} (hm : m ≠ 0) (h₁ : u₁ ⬝ᵥ u₁ = m) (h₁₂ : u₁ ⬝ᵥ u₂ = 0) (w : V → ℝ) : (w - (w ⬝ᵥ u₁ / m) • u₁ - (w ⬝ᵥ u₂ / m) • u₂) ⬝ᵥ u₁ = 0

theorem Averaging.residual_dotProduct_right {V : Type u_1} [Fintype V] {u₁ u₂ : V → ℝ} {m : ℝ} (hm : m ≠ 0) (h₂ : u₂ ⬝ᵥ u₂ = m) (h₁₂ : u₁ ⬝ᵥ u₂ = 0) (w : V → ℝ) : (w - (w ⬝ᵥ u₁ / m) • u₁ - (w ⬝ᵥ u₂ / m) • u₂) ⬝ᵥ u₂ = 0

theorem Averaging.residual_dotProduct_self {V : Type u_1} [Fintype V] {u₁ u₂ : V → ℝ} {m : ℝ} (hm : m ≠ 0) (h₁ : u₁ ⬝ᵥ u₁ = m) (h₂ : u₂ ⬝ᵥ u₂ = m) (h₁₂ : u₁ ⬝ᵥ u₂ = 0) (w : V → ℝ) : (w - (w ⬝ᵥ u₁ / m) • u₁ - (w ⬝ᵥ u₂ / m) • u₂) ⬝ᵥ (w - (w ⬝ᵥ u₁ / m) • u₁ - (w ⬝ᵥ u₂ / m) • u₂) = w ⬝ᵥ w - ((w ⬝ᵥ u₁) ^ 2 + (w ⬝ᵥ u₂) ^ 2) / m

theorem Averaging.sq_add_sq_le {V : Type u_1} [Fintype V] {u₁ u₂ : V → ℝ} {m : ℝ} (hm : 0 < m) (h₁ : u₁ ⬝ᵥ u₁ = m) (h₂ : u₂ ⬝ᵥ u₂ = m) (h₁₂ : u₁ ⬝ᵥ u₂ = 0) {w : V → ℝ} (hw : w ⬝ᵥ w = 1) : (w ⬝ᵥ u₁) ^ 2 + (w ⬝ᵥ u₂) ^ 2 ≤ m

A unit vector has squared projection on span {u₁, u₂} at most 1 (Bessel).

theorem Averaging.dotProduct_eq_zero_of_sq_add_sq_eq {V : Type u_1} [Fintype V] {u₁ u₂ : V → ℝ} {m : ℝ} (hm : 0 < m) (h₁ : u₁ ⬝ᵥ u₁ = m) (h₂ : u₂ ⬝ᵥ u₂ = m) (h₁₂ : u₁ ⬝ᵥ u₂ = 0) {w : V → ℝ} (hw : w ⬝ᵥ w = 1) (heq : (w ⬝ᵥ u₁) ^ 2 + (w ⬝ᵥ u₂) ^ 2 = m) {y : V → ℝ} (hy₁ : u₁ ⬝ᵥ y = 0) (hy₂ : u₂ ⬝ᵥ y = 0) : w ⬝ᵥ y = 0

Equality in Bessel's inequality: then w ∈ span {u₁, u₂}, so w ⊥ y whenever y ⊥ u₁, u₂.

theorem Averaging.pow_mulVec_dotProduct_self_le_of_orthogonal {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsHermitian) {lam c₁ c₂ m : ℝ} {u₁ u₂ : V → ℝ} (hK : {j : V | lam < |hA.eigenvalues j|}.card ≤ 2) (hc₁ : lam < |c₁|) (hc₂ : lam < |c₂|) (hu₁ : A.mulVec u₁ = c₁ • u₁) (hu₂ : A.mulVec u₂ = c₂ • u₂) (hm : 0 < m) (h₁ : u₁ ⬝ᵥ u₁ = m) (h₂ : u₂ ⬝ᵥ u₂ = m) (h₁₂ : u₁ ⬝ᵥ u₂ = 0) {y : V → ℝ} (hy₁ : u₁ ⬝ᵥ y = 0) (hy₂ : u₂ ⬝ᵥ y = 0) (t : ℕ) : (A ^ t).mulVec y ⬝ᵥ (A ^ t).mulVec y ≤ (lam ^ t) ^ 2 * y ⬝ᵥ y

Contraction off two eigenvectors. Let u₁, u₂ be orthogonal eigenvectors of A of equal squared norm m > 0, with eigenvalues c₁, c₂ exceeding λ in absolute value, and assume that at most two eigenvalues of A exceed λ in absolute value. Then ‖Aᵗ y‖² ≤ λ²ᵗ ‖y‖² for every y orthogonal to u₁ and u₂.