Spectral Theorem Formalization Challenges

“The spectral theorem has been formalized” is incomplete without its operator class and conclusion. Finite-dimensional diagonalization, the compact self-adjoint theorem, bounded functional calculus, and the unbounded projection-valued-measure theorem require different infrastructure. This page explains how to read or design such a formal statement. The mathematical proofs remain in the spectral chapter.

Required background. Projection-Valued Measures defines countable additivity; Unbounded Spectral Theorem specifies functional-calculus domains.

Identify the operator class before comparing theorems

A finite-dimensional self-adjoint theorem supplies an orthonormal basis of eigenvectors and real eigenvalues. A compact self-adjoint theorem extends a discrete eigenvector description under a compactness hypothesis. A general self-adjoint operator can have continuous spectrum and no eigenvectors at all, requiring a different output interface.

For example, Mathlib’s documented Mathlib.Analysis.InnerProductSpace.Spectrum contains finite-dimensional self-adjoint spectral results. The explicit finite-dimensional hypotheses are part of their meaning. A formal development using those declarations has not thereby established a theorem for every Schrödinger operator. Conversely, that file alone cannot establish the absence of more general results elsewhere; coverage is a revision-specific library question.

One should compare theorem statements, not search-result titles or the number of files containing the word “spectrum.”

A projection measure has an operator topology

For a self-adjoint operator $A$, a spectral measure $E$ assigns a bounded orthogonal projection to each Borel set. Its normalization and multiplication laws include

$$E(\mathbb R)=I,\qquad E(B\cap C)=E(B)E(C).$$

For disjoint Borel sets $(B_n)$, countable additivity means

$$E\!\left(\bigcup_nB_n\right)\psi =\sum_nE(B_n)\psi \qquad(\psi\in H),$$

with convergence in the Hilbert norm for each vector. This is strong operator additivity. Norm convergence of the projections is generally false. A formal measure interface using the operator norm without this qualification would encode an unnecessarily strong or incorrect theorem.

Scalar measures $\mu_\psi(B)=\langle\psi,E(B)\psi\rangle$ and their polarized counterparts connect the operator object to ordinary measure theory. The formal construction must establish positivity, countable additivity, and consistency across vectors, not just assign a scalar probability law separately for each state.

Measurable calculus must return a domain as well as an action

For a measurable function $f$, the operator $f(A)$ has domain

$$D(f(A))=\left\{\psi: \int|f(\lambda)|^2\,d\mu_\psi(\lambda)<\infty\right\}.$$

A useful formal interface therefore returns a partially defined operator with that domain, and states the topology in which bounded truncations converge to its action. A bounded Borel function produces an everywhere-defined bounded operator; a general function does not.

Equations between calculus expressions can also require domain comparisons. For example, the natural composition $f(A)g(A)$ can have a smaller domain than $(fg)(A)$ before taking a suitable closure or imposing additional conditions. A rewrite rule that erases this distinction is not the general unbounded functional calculus. Functions of Observables explains the underlying mathematics.

Finite expectation of an observable uses first-moment integrability, whereas membership in its operator domain uses a second moment. Formal types for expectation and operator application should not identify those two conditions merely because both are written with the symbol $A$.

A bounded transform does not remove endpoint obligations

A useful bridge from self-adjoint $A$ to a bounded operator is

$$T=A(I+A^2)^{-1/2}.$$

Its spectral function $t=\lambda/\sqrt{1+\lambda^2}$ lies in $(-1,1)$, and $\|T\|\le1$. Nevertheless the spectrum of $T$ can reach the endpoints $\pm1$ as limit points. Recovering $A$ uses the singular function $t/\sqrt{1-t^2}$ on $(-1,1)$ and its associated integrability domain. The spectral projections of $T$ at the endpoints vanish for this construction, but nearby spectral weight still determines an unbounded domain condition.

Thus a bounded-transform approach can organize a formal proof, but it does not make every recovery operation bounded. It must preserve the no-endpoint- eigenmass statement, the measurable calculus, and the exact recovered domain. These are substantive obligations rather than choices of notation.

Exercise: a bounded transform with norm one

Let $Ae_n=ne_n$ on its natural domain in $\ell^2(\mathbb N)$, with $n\ge1$. Compute $T$, its norm, and the domain obtained by applying the inverse spectral function to $T$. Is $1$ an eigenvalue of $T$?

Solution

The transformed eigenvalues are $t_n=n/\sqrt{1+n^2}<1$ and approach one, so $\|T\|=1$. No coordinate has eigenvalue one, hence $E_T(\{1\})=0$, although one belongs to the spectrum as a limit point. The inverse function gives $t_n/\sqrt{1-t_n^2}=n$. Its domain is $\{x:\sum_n n^2|x_n|^2<\infty\}$, exactly $D(A)$. Replacing the spectral bound by the false strict estimate $\|T\|<1$ would incorrectly make the inverse function bounded on the whole spectrum and lose the original domain.

References

• Hall, Brian C., Quantum Theory for Mathematicians, Graduate Texts in Mathematics 267, Springer, 2013, doi:10.1007/978-1-4614-7116-5 — spectral measures and unbounded functional calculus.
• Mathlib Contributors, Mathlib Documentation, “Spectral theorem for self-adjoint operators,” documented declarations — a concrete finite-dimensional theorem interface, with its hypotheses displayed.
• Teschl, Gerald, Mathematical Methods in Quantum Mechanics: With Applications to Schrödinger Operators, 2nd edition, Graduate Studies in Mathematics 157, American Mathematical Society, 2014, author PDF — functional calculus, domains, and self-adjoint spectral theory.