mathlib documentation

linear_algebra.matrix.spectrum

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

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

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

Equations
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
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) :

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

Equations
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
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
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) :
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) :

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.