# Documentation

Mathlib.LinearAlgebra.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 (LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply).

## Tags #

spectral theorem, diagonalization theorem

noncomputable def Matrix.IsHermitian.eigenvalues₀ {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :
Fin ()

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

Instances For
noncomputable def Matrix.IsHermitian.eigenvalues {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :
n

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

Instances For
noncomputable def Matrix.IsHermitian.eigenvectorBasis {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :

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

Instances For
noncomputable def Matrix.IsHermitian.eigenvectorMatrix {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :
Matrix n n 𝕜

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

Instances For
noncomputable def Matrix.IsHermitian.eigenvectorMatrixInv {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :
Matrix n n 𝕜

The inverse of eigenvectorMatrix

Instances For
theorem Matrix.IsHermitian.eigenvectorMatrix_mul_inv {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :
theorem Matrix.IsHermitian.eigenvectorMatrix_apply {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) (i : n) (j : n) :
theorem Matrix.IsHermitian.transpose_eigenvectorMatrix_apply {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) (i : n) :

The columns of Matrix.IsHermitian.eigenVectorMatrix form the basis

theorem Matrix.IsHermitian.eigenvectorMatrixInv_apply {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) (i : n) (j : n) :
= star ()
theorem Matrix.IsHermitian.conjTranspose_eigenvectorMatrixInv {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :
theorem Matrix.IsHermitian.conjTranspose_eigenvectorMatrix {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :
theorem Matrix.IsHermitian.spectral_theorem {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :
= Matrix.diagonal (IsROrC.ofReal ) *

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} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) (i : n) :
= IsROrC.re (Matrix.dotProduct () ())
theorem Matrix.IsHermitian.det_eq_prod_eigenvalues {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :
= Finset.prod Finset.univ fun i => ↑()

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

theorem Matrix.IsHermitian.spectral_theorem' {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :
A =

spectral theorem (Alternate form for convenience) A hermitian matrix can be can be replaced by a diagonal matrix sandwiched between the eigenvector matrices. This alternate form allows direct rewriting of A since: $A = V D V⁻¹$

theorem Matrix.IsHermitian.rank_eq_rank_diagonal {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :

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

theorem Matrix.IsHermitian.rank_eq_card_non_zero_eigs {𝕜 : Type u_1} [] [] {n : Type u_2} [] [] {A : Matrix n n 𝕜} (hA : ) :
= Fintype.card { i // }

rank of a hermitian matrix is the number of nonzero eigenvalues of the hermitian matrix