Spectral theory of self-adjoint operators #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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:
is_self_adjoint.conj_eigenvalue_eq_self: the eigenvalues are realis_self_adjoint.orthogonal_family_eigenspaces: the eigenspaces are orthogonalis_self_adjoint.orthogonal_supr_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
is_self_adjoint.diagonalizationprovides a linear isometry equivalenceEto the direct sum of the eigenspaces ofT. The theoremis_self_adjoint.diagonalization_apply_self_applystates that, whenTis transferred via this equivalence to an operator on the direct sum, it acts diagonally. - The definition
is_self_adjoint.eigenvector_basisprovides an orthonormal basis forEconsisting of eigenvectors ofT, withis_self_adjoint.eigenvaluesgiving the corresponding list of eigenvalues, as real numbers. The definitionis_self_adjoint.diagonalization_basisgives the associated linear isometry equivalence fromEto Euclidean space, and the theoremis_self_adjoint.diagonalization_basis_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
- linear_map.is_symmetric.direct_sum_decomposition = linear_map.is_symmetric.direct_sum_decomposition._proof_3.decomposition linear_map.is_symmetric.direct_sum_decomposition._proof_4
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
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.
Equations
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.
Equations
- hT.eigenvalues hn i = ⇑is_R_or_C.re ↑(direct_sum.is_internal.subordinate_orthonormal_basis_index hn _ i _)
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.