Spectral theory of hermitian matrices

This file proves the spectral theorem for matrices. The proof of the spectral theorem is based on the spectral theorem for linear maps (LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply).

Tags

spectral theorem, diagonalization theorem

noncomputable def Matrix.IsHermitian.eigenvalues₀ {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : Fin (Fintype.card n) → ℝ

The eigenvalues of a hermitian matrix, indexed by Fin (Fintype.card n) where n is the index type of the matrix.

Equations

• hA.eigenvalues₀ = ⋯.eigenvalues ⋯

noncomputable def Matrix.IsHermitian.eigenvalues {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : n → ℝ

The eigenvalues of a hermitian matrix, reusing the index n of the matrix entries.

Equations

• hA.eigenvalues i = hA.eigenvalues₀ ((Fintype.equivOfCardEq ⋯).symm i)

noncomputable def Matrix.IsHermitian.eigenvectorBasis {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)

A choice of an orthonormal basis of eigenvectors of a hermitian matrix.

Equations

• hA.eigenvectorBasis = (⋯.eigenvectorBasis ⋯).reindex (Fintype.equivOfCardEq ⋯)

noncomputable def Matrix.IsHermitian.eigenvectorMatrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : Matrix n n 𝕜

A matrix whose columns are an orthonormal basis of eigenvectors of a hermitian matrix.

Equations

• hA.eigenvectorMatrix = (PiLp.basisFun 2 𝕜 n).toMatrix ⇑hA.eigenvectorBasis.toBasis

noncomputable def Matrix.IsHermitian.eigenvectorMatrixInv {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : Matrix n n 𝕜

The inverse of eigenvectorMatrix

Equations

• hA.eigenvectorMatrixInv = hA.eigenvectorBasis.toBasis.toMatrix ⇑(PiLp.basisFun 2 𝕜 n)

theorem Matrix.IsHermitian.eigenvectorMatrix_mul_inv {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : hA.eigenvectorMatrix * hA.eigenvectorMatrixInv = 1

noncomputable instance Matrix.IsHermitian.instInvertibleEigenvectorMatrixInv {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : Invertible hA.eigenvectorMatrixInv

Equations

• hA.instInvertibleEigenvectorMatrixInv = hA.eigenvectorMatrixInv.invertibleOfLeftInverse hA.eigenvectorMatrix ⋯

noncomputable instance Matrix.IsHermitian.instInvertibleEigenvectorMatrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : Invertible hA.eigenvectorMatrix

Equations

• hA.instInvertibleEigenvectorMatrix = hA.eigenvectorMatrix.invertibleOfRightInverse hA.eigenvectorMatrixInv ⋯

theorem Matrix.IsHermitian.eigenvectorMatrix_apply {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (i : n) (j : n) : hA.eigenvectorMatrix i j = hA.eigenvectorBasis j i

theorem Matrix.IsHermitian.transpose_eigenvectorMatrix_apply {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (i : n) : hA.eigenvectorMatrix.transpose i = hA.eigenvectorBasis i

The columns of Matrix.IsHermitian.eigenVectorMatrix form the basis

theorem Matrix.IsHermitian.eigenvectorMatrixInv_apply {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (i : n) (j : n) : hA.eigenvectorMatrixInv i j = star (hA.eigenvectorBasis i j)

theorem Matrix.IsHermitian.conjTranspose_eigenvectorMatrixInv {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : hA.eigenvectorMatrixInv.conjTranspose = hA.eigenvectorMatrix

theorem Matrix.IsHermitian.conjTranspose_eigenvectorMatrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : hA.eigenvectorMatrix.conjTranspose = hA.eigenvectorMatrixInv

theorem Matrix.IsHermitian.spectral_theorem {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : hA.eigenvectorMatrixInv * A = Matrix.diagonal (RCLike.ofReal ∘ hA.eigenvalues) * hA.eigenvectorMatrixInv

Diagonalization theorem, spectral theorem for matrices; A hermitian matrix can be diagonalized by a change of basis.

For the spectral theorem on linear maps, see LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply.

theorem Matrix.IsHermitian.eigenvalues_eq {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (i : n) : hA.eigenvalues i = RCLike.re (Matrix.dotProduct (star (hA.eigenvectorMatrix.transpose i)) (A.mulVec (hA.eigenvectorMatrix.transpose i)))

theorem Matrix.IsHermitian.det_eq_prod_eigenvalues {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : A.det = Finset.univ.prod fun (i : n) => ↑(hA.eigenvalues i)

The determinant of a hermitian matrix is the product of its eigenvalues.

theorem Matrix.IsHermitian.spectral_theorem' {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : A = hA.eigenvectorMatrix * Matrix.diagonal (RCLike.ofReal ∘ hA.eigenvalues) * hA.eigenvectorMatrixInv

spectral theorem (Alternate form for convenience) A hermitian matrix can be can be replaced by a diagonal matrix sandwiched between the eigenvector matrices. This alternate form allows direct rewriting of A since: <| A = V D V⁻¹$

theorem Matrix.IsHermitian.rank_eq_rank_diagonal {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : A.rank = (Matrix.diagonal hA.eigenvalues).rank

rank of a hermitian matrix is the rank of after diagonalization by the eigenvector matrix

theorem Matrix.IsHermitian.rank_eq_card_non_zero_eigs {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : A.rank = Fintype.card { i : n // hA.eigenvalues i ≠ 0 }

rank of a hermitian matrix is the number of nonzero eigenvalues of the hermitian matrix

theorem Matrix.IsHermitian.mulVec_eigenvectorBasis {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (i : n) : A.mulVec (hA.eigenvectorBasis i) = hA.eigenvalues i • hA.eigenvectorBasis i

The entries of eigenvectorBasis are eigenvectors.

theorem Matrix.IsHermitian.exists_eigenvector_of_ne_zero {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) (h_ne : A ≠ 0) : ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A.mulVec v = t • v

A nonzero Hermitian matrix has an eigenvector with nonzero eigenvalue.