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
The eigenvalues of a hermitian matrix, indexed by Fin (Fintype.card n)
where n
is the index
type of the matrix.
Instances For
The eigenvalues of a hermitian matrix, reusing the index n
of the matrix entries.
Instances For
A choice of an orthonormal basis of eigenvectors of a hermitian matrix.
Instances For
A matrix whose columns are an orthonormal basis of eigenvectors of a hermitian matrix.
Instances For
The inverse of eigenvectorMatrix
Instances For
The columns of Matrix.IsHermitian.eigenVectorMatrix
form the basis
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
.
The determinant of a hermitian matrix is the product of its eigenvalues.
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⁻¹$
rank of a hermitian matrix is the rank of after diagonalization by the eigenvector matrix
rank of a hermitian matrix is the number of nonzero eigenvalues of the hermitian matrix