# mathlib3documentation

linear_algebra.matrix.spectrum

# 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

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 : 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 : n 𝕜} (hA : A.is_hermitian) :

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 : n 𝕜} (hA : A.is_hermitian) :
n)

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 : n 𝕜} (hA : A.is_hermitian) :
n 𝕜

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

Equations
Instances for matrix.is_hermitian.eigenvector_matrix
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 : n 𝕜} (hA : A.is_hermitian) :
n 𝕜

The inverse of eigenvector_matrix

Equations
Instances for matrix.is_hermitian.eigenvector_matrix_inv
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 : n 𝕜} (hA : A.is_hermitian) :
@[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 : n 𝕜} (hA : A.is_hermitian) :
Equations
@[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 : n 𝕜} (hA : A.is_hermitian) :
Equations
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 : n 𝕜} (hA : A.is_hermitian) (i j : n) :
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 : n 𝕜} (hA : A.is_hermitian) (i j : n) :
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 : n 𝕜} (hA : A.is_hermitian) :
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 : 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 : 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.

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 : n 𝕜} (hA : A.is_hermitian) (i : n) :
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 : 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.