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
The eigenvalues of a hermitian matrix, indexed by fin (fintype.card n)
where n
is the index
type of the matrix.
Equations
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)
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_15)
A matrix whose columns are an orthonormal basis of eigenvectors of a hermitian matrix.
Equations
- hA.eigenvector_matrix = (pi.basis_fun 𝕜 n).to_matrix ⇑(hA.eigenvector_basis.to_basis)
The inverse of eigenvector_matrix
Equations
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
.