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 (diagonalization_basis_apply_self_apply).

Tags #

spectral theorem, diagonalization theorem

source

noncomputable def matrix.is_hermitian.eigenvalues₀ {𝕜 : Type u_1} [is_R_or_C 𝕜] [decidable_eq 𝕜] {n : Type u_2} [fintype n] [decidable_eq n] {A : matrix n n 𝕜} (hA : A.is_hermitian) :

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 finrank_euclidean_space

source

noncomputable def matrix.is_hermitian.eigenvalues {𝕜 : Type u_1} [is_R_or_C 𝕜] [decidable_eq 𝕜] {n : Type u_2} [fintype n] [decidable_eq n] {A : matrix n n 𝕜} (hA : A.is_hermitian) :

n → ℝ

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

Equations

hA.eigenvalues = λ (i : n), hA.eigenvalues₀ (⇑((fintype.equiv_of_card_eq matrix.is_hermitian.eigenvalues._proof_1).symm) i)

source

noncomputable def matrix.is_hermitian.eigenvector_basis {𝕜 : Type u_1} [is_R_or_C 𝕜] [decidable_eq 𝕜] {n : Type u_2} [fintype n] [decidable_eq n] {A : matrix n n 𝕜} (hA : A.is_hermitian) :

orthonormal_basis n 𝕜 (euclidean_space 𝕜 n)

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

Equations

hA.eigenvector_basis = (_.eigenvector_basis finrank_euclidean_space).reindex (fintype.equiv_of_card_eq matrix.is_hermitian.eigenvector_basis._proof_15)

source

noncomputable def matrix.is_hermitian.eigenvector_matrix {𝕜 : Type u_1} [is_R_or_C 𝕜] [decidable_eq 𝕜] {n : Type u_2} [fintype n] [decidable_eq n] {A : matrix n n 𝕜} (hA : A.is_hermitian) :

matrix n n 𝕜

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

Equations

hA.eigenvector_matrix = (pi.basis_fun 𝕜 n).to_matrix ⇑(hA.eigenvector_basis.to_basis)

source

noncomputable def matrix.is_hermitian.eigenvector_matrix_inv {𝕜 : Type u_1} [is_R_or_C 𝕜] [decidable_eq 𝕜] {n : Type u_2} [fintype n] [decidable_eq n] {A : matrix n n 𝕜} (hA : A.is_hermitian) :

matrix n n 𝕜

The inverse of eigenvector_matrix

Equations

hA.eigenvector_matrix_inv = hA.eigenvector_basis.to_basis.to_matrix ⇑(pi.basis_fun 𝕜 n)

source

theorem matrix.is_hermitian.eigenvector_matrix_mul_inv {𝕜 : Type u_1} [is_R_or_C 𝕜] [decidable_eq 𝕜] {n : Type u_2} [fintype n] [decidable_eq n] {A : matrix n n 𝕜} (hA : A.is_hermitian) :

hA.eigenvector_matrix.mul hA.eigenvector_matrix_inv = 1

source

theorem matrix.is_hermitian.spectral_theorem {𝕜 : Type u_1} [is_R_or_C 𝕜] [decidable_eq 𝕜] {n : Type u_2} [fintype n] [decidable_eq n] {A : matrix n n 𝕜} (hA : A.is_hermitian) :

hA.eigenvector_matrix_inv.mul A = (matrix.diagonal (coe ∘ hA.eigenvalues)).mul hA.eigenvector_matrix_inv

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