Spectral decompositions of self-adjoint operators #
Mathlib's spectral theorem for a compact self-adjoint operator T on a Hilbert space E says
that the eigenspaces of T have trivial mutual orthogonal complement
(ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot) and that the eigenspaces at
nonzero eigenvalues are finite dimensional
(ContinuousLinearMap.finite_dimensional_eigenspace). This file turns the first statement into
the form the applications want: E has an orthonormal basis consisting of eigenvectors of
T.
The construction is the classical one. Each eigenspace is closed, hence a Hilbert space in its
own right, so it has a Hilbert basis; the eigenspaces are mutually orthogonal, so the union of
those bases is an orthonormal family; and a vector orthogonal to the whole family is orthogonal
to every eigenspace, hence zero. HilbertBasis.mkOfOrthogonalEqBot then assembles the family
into a Hilbert basis of E.
In finite dimensions, this file also packages Mathlib's ordered eigenbasis into the spans of any chosen set of its eigenvectors. In particular, the negative and positive spectral subspaces, spanned by the eigenvectors with negative and with positive eigenvalue, are disjoint, invariant under the operator, and together span the whole space when the operator is injective.
No separability is assumed anywhere: the basis is indexed by a set of vectors of E, exactly as
in Mathlib's exists_hilbertBasis, and the eigenvalue 0 may well carry an infinite-dimensional
eigenspace. When T is injective that eigenspace is trivial and every basis vector has a
nonzero eigenvalue, which is the form the eigenvalue problem of an elliptic operator uses.
Main declarations #
ContinuousLinearMap.exists_hilbertBasis_forall_hasEigenvector_of_dense_eigenspaces: a symmetric operator whose eigenspaces have dense span admits a Hilbert basis of eigenvectors.ContinuousLinearMap.exists_hilbertBasis_forall_hasEigenvector: the compact symmetric specialization of the preceding result.ContinuousLinearMap.exists_hilbertBasis_forall_hasEigenvector_ne_zero: for an injective compact symmetric operator, every vector of that basis has a nonzero eigenvalue.ContinuousLinearMap.hasSum_smul_repr_of_apply_eq_smul: an operator diagonal in a Hilbert basis is the sum of its eigencomponents, the spectral expansion such a basis is for.LinearMap.IsSymmetric.eigenvectorSpan: the span of the eigenvectors of the ordered eigenbasis whose indices lie in a specified set.LinearMap.IsSymmetric.negativeSpectralSubspaceandLinearMap.IsSymmetric.positiveSpectralSubspace: the negative and positive halves of the finite-dimensional spectral splitting.
References #
H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Theorem 6.11 (the Hilbert--Schmidt spectral decomposition); L. C. Evans, Partial Differential Equations, Appendix D.6.
A symmetric operator whose eigenspaces have dense span has an orthonormal basis of
eigenvectors. The basis is indexed by a set of vectors of E, as in exists_hilbertBasis,
and no separability is assumed.
A compact self-adjoint operator has an orthonormal basis of eigenvectors.
An injective symmetric operator whose eigenspaces have dense span has an orthonormal basis of eigenvectors with nonzero eigenvalues.
An injective compact self-adjoint operator has an orthonormal basis of eigenvectors with
nonzero eigenvalues. Injectivity excludes the eigenvalue 0.
The spectral expansion of an operator diagonal in a Hilbert basis. Applying T term by
term to the expansion of y writes T y as the sum of its eigencomponents; combined with
ContinuousLinearMap.exists_hilbertBasis_forall_hasEigenvector this diagonalizes a compact
self-adjoint operator.
Finite-dimensional eigenvector spans #
The span of the eigenvectors whose indices belong to s.
The eigenvectors are those of Mathlib's decreasingly ordered eigenbasis, so this span depends on that basis and may select only part of a repeated eigenspace. It is particularly useful with subsets cut out by inequalities on the corresponding eigenvalues.
Equations
- hT.eigenvectorSpan hn s = Submodule.span 𝕜 (⇑(hT.eigenvectorBasis hn) '' s)
Instances For
A vector belongs to an eigenvector span exactly when its eigenbasis representation is supported on the selected indices.
An eigenvector from the ordered eigenbasis belongs to an eigenvector span exactly when its index is selected.
Enlarging the set of eigenvector indices enlarges its span.
The eigenvector span of a union is the sum of the two eigenvector spans.
The eigenvector span of the empty set is zero.
All eigenvectors together span the whole finite-dimensional inner product space.
Eigenvector spans indexed by disjoint sets are disjoint.
The dimension of an eigenvector span is the number of eigenvectors selected.
A symmetric operator preserves each of its eigenvector spans.
The negative spectral subspace of a finite-dimensional symmetric operator: the span of the eigenvectors with negative eigenvalue.
Equations
- hT.negativeSpectralSubspace hn = hT.eigenvectorSpan hn {i : Fin n | hT.eigenvalues hn i < 0}
Instances For
The positive spectral subspace of a finite-dimensional symmetric operator: the span of the eigenvectors with positive eigenvalue.
Equations
- hT.positiveSpectralSubspace hn = hT.eigenvectorSpan hn {i : Fin n | 0 < hT.eigenvalues hn i}
Instances For
A vector belongs to the negative spectral subspace exactly when its eigenbasis representation is supported on the negative eigenvalues.
A vector belongs to the positive spectral subspace exactly when its eigenbasis representation is supported on the positive eigenvalues.
The dimension of the negative spectral subspace counts the negative eigenvalues, with multiplicity.
The dimension of the positive spectral subspace counts the positive eigenvalues, with multiplicity.
A symmetric operator preserves its negative spectral subspace.
A symmetric operator preserves its positive spectral subspace.
The negative and positive spectral subspaces are disjoint.
An injective symmetric operator has no zero eigenvalue in its ordered eigenvalue family.
For an injective symmetric operator, its negative and positive spectral subspaces are complementary: they are disjoint and together span the whole space.