Spectral theory of hermitian matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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_Lp.basis_fun 2 𝕜 n).to_matrix ⇑(hA.eigenvector_basis.to_basis)

Instances for matrix.is_hermitian.eigenvector_matrix

matrix.is_hermitian.eigenvector_matrix.invertible

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_Lp.basis_fun 2 𝕜 n)

Instances for matrix.is_hermitian.eigenvector_matrix_inv

matrix.is_hermitian.eigenvector_matrix_inv.invertible

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

@[protected, instance]

noncomputable def matrix.is_hermitian.eigenvector_matrix_inv.invertible {𝕜 : 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) :

invertible hA.eigenvector_matrix_inv

Equations

matrix.is_hermitian.eigenvector_matrix_inv.invertible hA = hA.eigenvector_matrix_inv.invertible_of_left_inverse hA.eigenvector_matrix _

source

@[protected, instance]

noncomputable def matrix.is_hermitian.eigenvector_matrix.invertible {𝕜 : 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) :

invertible hA.eigenvector_matrix

Equations

matrix.is_hermitian.eigenvector_matrix.invertible hA = hA.eigenvector_matrix.invertible_of_right_inverse hA.eigenvector_matrix_inv _

source

theorem matrix.is_hermitian.eigenvector_matrix_apply {𝕜 : 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) (i j : n) :

hA.eigenvector_matrix i j = ⇑(hA.eigenvector_basis) j i

source

theorem matrix.is_hermitian.eigenvector_matrix_inv_apply {𝕜 : 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) (i j : n) :

hA.eigenvector_matrix_inv i j = has_star.star (⇑(hA.eigenvector_basis) i j)

source

theorem matrix.is_hermitian.conj_transpose_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) :

hA.eigenvector_matrix_inv.conj_transpose = hA.eigenvector_matrix

source

theorem matrix.is_hermitian.conj_transpose_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) :

hA.eigenvector_matrix.conj_transpose = hA.eigenvector_matrix_inv

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.

source

theorem matrix.is_hermitian.eigenvalues_eq {𝕜 : 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) (i : n) :

hA.eigenvalues i = ⇑is_R_or_C.re (matrix.dot_product (has_star.star (hA.eigenvector_matrix.transpose i)) (A.mul_vec (hA.eigenvector_matrix.transpose i)))

source

theorem matrix.is_hermitian.det_eq_prod_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) :

A.det = finset.univ.prod (λ (i : n), ↑(hA.eigenvalues i))

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