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 ⋯)

theorem Matrix.IsHermitian.mulVec_eigenvectorBasis {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (j : n) : A.mulVec ((WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis j)) = hA.eigenvalues j • (WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis j)

theorem Matrix.IsHermitian.spectrum_toEuclideanLin {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] : spectrum 𝕜 (toEuclideanLin A) = spectrum 𝕜 A

The spectrum of a Hermitian matrix A coincides with the spectrum of toEuclideanLin A.

theorem Matrix.IsHermitian.eigenvalues_mem_spectrum_real {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (i : n) : hA.eigenvalues i ∈ spectrum ℝ A

Eigenvalues of a hermitian matrix A are in the ℝ spectrum of A.

noncomputable def Matrix.IsHermitian.eigenvectorUnitary {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_4} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : ↥(unitaryGroup n 𝕜)

Unitary matrix whose columns are Matrix.IsHermitian.eigenvectorBasis.

Equations

• hA.eigenvectorUnitary = ⟨(EuclideanSpace.basisFun n 𝕜).toBasis.toMatrix ⇑hA.eigenvectorBasis.toBasis, ⋯⟩

theorem Matrix.IsHermitian.eigenvectorUnitary_coe {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_4} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : ↑hA.eigenvectorUnitary = (EuclideanSpace.basisFun n 𝕜).toBasis.toMatrix ⇑hA.eigenvectorBasis.toBasis

@[simp]

theorem Matrix.IsHermitian.eigenvectorUnitary_transpose_apply {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (j : n) : (↑hA.eigenvectorUnitary).transpose j = (WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis j)

@[simp]

theorem Matrix.IsHermitian.eigenvectorUnitary_apply {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (i j : n) : ↑hA.eigenvectorUnitary i j = (WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis j) i

theorem Matrix.IsHermitian.eigenvectorUnitary_mulVec {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (j : n) : (↑hA.eigenvectorUnitary).mulVec (Pi.single j 1) = (WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis j)

theorem Matrix.IsHermitian.star_eigenvectorUnitary_mulVec {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (j : n) : (star ↑hA.eigenvectorUnitary).mulVec ((WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis j)) = Pi.single j 1

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

Unitary diagonalization of a Hermitian matrix.

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.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary

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 (star ((WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis i)) ⬝ᵥ A.mulVec ((WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis 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 = ∏ i : n, ↑(hA.eigenvalues i)

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

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 = (diagonal hA.eigenvalues).rank

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

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.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.