Spectral theory of self-adjoint operators #
This file covers the spectral theory of self-adjoint operators on an inner product space.
The first part of the file covers general properties, true without any condition on boundedness or compactness of the operator or finite-dimensionality of the underlying space, notably:
LinearMap.IsSymmetric.conj_eigenvalue_eq_self: the eigenvalues are realLinearMap.IsSymmetric.orthogonalFamily_eigenspaces: the eigenspaces are orthogonalLinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces: the restriction of the operator to the mutual orthogonal complement of the eigenspaces has, itself, no eigenvectors
The second part of the file covers properties of self-adjoint operators in finite dimension.
Letting T be a self-adjoint operator on a finite-dimensional inner product space T,
- The definition
LinearMap.IsSymmetric.diagonalizationprovides a linear isometry equivalenceEto the direct sum of the eigenspaces ofT. The theoremLinearMap.IsSymmetric.diagonalization_apply_self_applystates that, whenTis transferred via this equivalence to an operator on the direct sum, it acts diagonally. - The definition
LinearMap.IsSymmetric.eigenvectorBasisprovides an orthonormal basis forEconsisting of eigenvectors ofT, withLinearMap.IsSymmetric.eigenvaluesgiving the corresponding list of eigenvalues, as real numbers. The definitionLinearMap.IsSymmetric.eigenvectorBasisgives the associated linear isometry equivalence fromEto Euclidean space, and the theoremLinearMap.IsSymmetric.eigenvectorBasis_apply_self_applystates that, whenTis transferred via this equivalence to an operator on Euclidean space, it acts diagonally.
These are forms of the diagonalization theorem for self-adjoint operators on finite-dimensional inner product spaces.
TODO #
Spectral theory for compact self-adjoint operators, bounded self-adjoint operators.
Tags #
self-adjoint operator, spectral theorem, diagonalization theorem
A self-adjoint operator preserves orthogonal complements of its eigenspaces.
The eigenvalues of a self-adjoint operator are real.
The eigenspaces of a self-adjoint operator are mutually orthogonal.
The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on an inner product space is an invariant subspace of the operator.
The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on an inner product space has no eigenvalues.
Finite-dimensional theory #
The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on a finite-dimensional inner product space is trivial.
The eigenspaces of a self-adjoint operator on a finite-dimensional inner product space E gives
an internal direct sum decomposition of E.
Note this takes hT as a Fact to allow it to be an instance.
Equations
- LinearMap.IsSymmetric.directSumDecomposition = โฏ.decomposition โฏ
The eigenspaces of a self-adjoint operator on a finite-dimensional inner product space E gives
an internal direct sum decomposition of E.
Isometry from an inner product space E to the direct sum of the eigenspaces of some
self-adjoint operator T on E.
Equations
- hT.diagonalization = โฏ.isometryL2OfOrthogonalFamily โฏ
Instances For
Diagonalization theorem, spectral theorem; version 1: A self-adjoint operator T on a
finite-dimensional inner product space E acts diagonally on the decomposition of E into the
direct sum of the eigenspaces of T.
A choice of orthonormal basis of eigenvectors for self-adjoint operator T on a
finite-dimensional inner product space E.
TODO Postcompose with a permutation so that these eigenvectors are listed in increasing order of eigenvalue.
Instances For
The sequence of real eigenvalues associated to the standard orthonormal basis of eigenvectors
for a self-adjoint operator T on E.
TODO Postcompose with a permutation so that these eigenvalues are listed in increasing order.
Instances For
Diagonalization theorem, spectral theorem; version 2: A self-adjoint operator T on a
finite-dimensional inner product space E acts diagonally on the identification of E with
Euclidean space induced by an orthonormal basis of eigenvectors of T.