Hilbert Space Formalization Challenges

Passing from matrices to general Hilbert spaces changes the objects a formal development must represent. Vectors may be equivalence classes of functions; operators may have proper dense domains; tensor products require completion; and a limit must name its topology. These are mathematical interfaces, not syntax obstacles. A useful formalization preserves the distinctions that make infinite-dimensional theorems true.

Required background. Hilbert Space as State Space explains completeness; Dense Domains and Closed and Closable Operators specify partial operators and graph closure.

Completeness is a hypothesis with consequences

An inner-product space need not be complete. Hilbert-space results that use Riesz representation, orthogonal projection onto a closed subspace, or limits of Cauchy sequences require completeness where it is invoked. A formal library may carry completeness as an additional structure rather than including it in every inner-product-space type.

The distinction should remain visible at the boundary of a theorem. Completing an algebraic space is a construction with a dense isometric embedding, not merely renaming it. Extending an operator through that embedding requires a continuity estimate and uniqueness on the dense subspace. Algebraic Tensor Products and Completion provides an important quantum example.

Separability is separate again. It permits countable bases and convenient sequence descriptions, but is not part of the definition of every Hilbert space. A formalization should not import it through a coordinate representation unless the theorem actually assumes it.

An L² vector is not a pointwise function

An $L^2$ vector is an almost-everywhere equivalence class. A construction on representatives descends to the quotient only after proving that it is independent of the representative. The inner product does descend; evaluation at a fixed point generally does not.

Consequently, a theorem that contains $\psi(x_0)$ needs extra structure: for example a continuous representative in a suitable Sobolev or test space. Selecting an arbitrary representative does not make point evaluation a well-defined physical observable on $L^2$. The position-ket treatment explains the correct generalized-functional setting.

Weak derivatives add another layer. The domain of a differential operator must encode existence of the appropriate distributional derivative and its integrability. A proof about smooth functions can be a first step, but extension to a Sobolev domain requires an actual density or closure theorem.

A partial operator carries its domain

An unbounded operator can be represented by a linear subspace $D(A)$ and a linear map from that subspace to $H$, or by an equivalent graph-based structure. Equality of operators then requires equality of domains as well as equality of values. Composition has domain

$$D(AB)=\{\psi\in D(B):B\psi\in D(A)\}.$$

This dependent membership condition is why manipulating $AB-BA$ as if both were everywhere-defined matrices loses essential information. Formalizing the expression should require a proof that every application is meaningful, or specify an agreed common domain explicitly.

Mathlib’s partially defined linear-map documentation illustrates one possible interface. Its existence does not certify that every desired unbounded-operator theorem is available; theorem coverage must be checked at the selected library revision.

Adjoints require density and graph norms require closure

For a densely defined operator, the adjoint pairs vectors through an inner-product identity. Density makes the representing vector unique. Without it, a relation can be more natural than a single-valued adjoint. The unbounded adjoint article proves that theorem; a formal interface must retain its density premise.

For a closed operator, equip its domain with

$$\|\psi\|_A^2=\|\psi\|^2+\|A\psi\|^2.$$

The resulting domain is complete, and $A:D(A)\to H$ is bounded when the input carries this graph norm. This does not make $A$ bounded on $H$ with its original norm. The formal domain type and its norm are part of the statement. Reusing the same symbol for two normed spaces can hide a false application of the closed graph theorem.

Infinite limits need a declared topology

A sequence of operators can converge strongly without converging in operator norm. A sequence of vectors can converge weakly without preserving norms. A sequence of finite-rank states can converge in trace norm while their entropies behave discontinuously. The corresponding formal limits are different propositions with different hypotheses.

One useful design is to establish convergence in the weakest topology that the next argument needs, then invoke a separate theorem for any stronger conclusion. Tracking Topologies gives the mathematical examples. Merely replacing an infinite object by larger matrices does not certify convergence of its domains, spectrum, or entropy.

Exercise: identify the norm in a boundedness claim

On $\ell^2(\mathbb N)$, let $Ae_n=ne_n$ with domain $\{x:\sum_n n^2|x_n|^2<\infty\}$. Explain why its graph-domain map is bounded but no uniform bound $\|Ax\|\le C\|x\|$ holds on that domain with the ambient norm.

Solution

The graph norm gives $\|Ax\|\le\|x\|_A$ directly, so the first map has operator norm at most one. For the ambient norm, the unit vectors satisfy $\|e_n\|=1$ and $\|Ae_n\|=n$, contradicting every finite constant $C$. The algebraic action and vector set are the same, but the norm on the input space has changed. A formal proof must identify that norm before calling either map continuous.

References

• Hall, Brian C., Quantum Theory for Mathematicians, Graduate Texts in Mathematics 267, Springer, 2013, doi:10.1007/978-1-4614-7116-5 — Hilbert spaces, domains, and unbounded adjoints.
• Mathlib Contributors, Mathlib Documentation, “Partially defined linear maps” and “Adjoints of partially defined linear maps,” linear maps, adjoints — concrete interface examples; declarations and coverage depend on the library revision.
• Unruh, Dominique, “Quantum and Classical Registers,” Archive of Formal Proofs, 28 October 2021, formal development — subsystem abstractions built on Hilbert-space tensor infrastructure.