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) :
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
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, 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)
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)
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
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
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
@[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) :
@[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) :
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
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)
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) :
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) :
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.
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)))
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.