Theorem 2.26 — self-adjoint extensions exist iff the defect indices are equal

Proved

TeschlQM.SelfAdjoint.selfAdjoint_extension_iff

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

defect-indicesextensionsfunctional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1self-adjoint-operators

Let $A$ be a symmetric operator on a complex Hilbert space $\mathfrak{H}$ , with defect spaces $K_\pm = \operatorname{Ran}(A \pm \mathrm{i})^\perp$ and defect indices $d_\pm(A) = \dim K_\pm$ . Then $A$ has a self-adjoint extension, that is a self-adjoint $B$ with $\mathfrak{D}(A) \subseteq \mathfrak{D}(B)$ and $B = A$ on $\mathfrak{D}(A)$ , if and only if

d_+(A) = d_-(A).

This is von Neumann's criterion. It decides whether a formal quantum-mechanical Hamiltonian given on a convenient domain can be turned into a genuine observable at all, and it is the starting point for classifying all such realizations.

Formalization Note. Operators are LinearPMaps; extension is A ≤ B; self-adjointness is Mathlib's IsSelfAdjoint. Symmetric includes a dense domain, so $A^*$ is the book's adjoint. $K_\pm$ are defined as $\operatorname{Ran}(A \pm \mathrm{i})^\perp$ , not as kernels of $A \mp \mathrm{i}$ (which are trivial for symmetric $A$ ). Equality of the Hilbert dimensions $d_\pm$ is expressed as the existence of a unitary (surjective linear isometry) $K_+ \to K_-$ . No separability of $\mathfrak{H}$ is assumed; the statement holds for every complex Hilbert space.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_IsSymmetric
import Definitions.Def_TeschlQM_SelfAdjoint_defectSpace

Formal statement

namespace TeschlQM.SelfAdjoint

/-- Teschl, Theorem 2.26, first sentence (p. 82): a symmetric operator has self-adjoint extensions
if and only if its defect indices are equal. An extension `B ⊇ A` is `A ≤ B` (`𝔇(A) ⊆ 𝔇(B)`
and `B = A` on `𝔇(A)`); equality of `d₊ = dim Ran(A + i)^⊥` and `d₋ = dim Ran(A - i)^⊥` is the
existence of a unitary between the two defect spaces. -/
theorem selfAdjoint_extension_iff {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (A : H →ₗ.[ℂ] H) (hA : TeschlQM.Shared.IsSymmetric A) :
    (∃ B : H →ₗ.[ℂ] H, A ≤ B ∧ IsSelfAdjoint B) ↔ HasEqualDefectIndices A := by sorry

end TeschlQM.SelfAdjoint

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 82, Theorem 2.26

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $H$ be a complex Hilbert space: a complex inner product space $(H, \langle\cdot,\cdot\rangle)$ that is complete in its norm. No separability is assumed, and $H$ may be the zero space. Let $A$ be a partially defined linear operator on $H$ . That is, $A$ has a domain $\mathfrak{D}(A)$ , which is some complex linear subspace of $H$ , and $A$ is a $\mathbb{C}$ -linear map $\mathfrak{D}(A) \to H$ . Nothing in the statement requires $\mathfrak{D}(A)$ to be dense or closed, or requires $A$ to be closed or bounded. Assume the hypothesis

\mathrm{IsSymmetric}(A),

where $\mathrm{IsSymmetric}$ is a predicate defined elsewhere in this bundle (TeschlQM.Shared.IsSymmetric). Its definition is not shown in the code I was given, so I cannot unfold it here. Whether it includes density of $\mathfrak{D}(A)$ or the symmetry condition $\langle Ax, y\rangle = \langle x, Ay\rangle$ for $x, y \in \mathfrak{D}(A)$ has to be checked in that definition.

The statement asserts the following equivalence:

\Big(\exists\, B:\ A \le B \ \text{ and } \ B^* = B\Big) \iff \mathrm{HasEqualDefectIndices}(A).

$B$ : $B$ ranges over all partially defined $\mathbb{C}$ -linear operators on $H$ .
$A \le B$ : $B$ extends $A$ . This means $\mathfrak{D}(A) \subseteq \mathfrak{D}(B)$ and $Bx = Ax$ for every $x \in \mathfrak{D}(A)$ .
$B^* = B$ : $B$ $B$ is self-adjoint in the sense of the library's adjoint of partially defined operators. $B$ $B$ must equal its adjoint $B^*$ $B^{*}$ , with the same domain and the same values.
- The domain of $B^*$ is the set of $y \in H$ for which $x \mapsto \langle y, Bx\rangle$ is continuous on $\mathfrak{D}(B)$ .
- When $\mathfrak{D}(B)$ is dense, $B^*y$ is the usual adjoint vector.
- When $\mathfrak{D}(B)$ is not dense, the library defines $B^*$ as the zero map on that domain.
- For $H \ne \{0\}$ , the library shows that a self-adjoint operator in this sense has a dense domain.
$\mathrm{HasEqualDefectIndices}(A)$ : another predicate defined elsewhere in this bundle. Judging by its imports, it is presumably built on the bundle's defectSpace definition, but its definition is not shown in the code I was given. The Lean comment above the theorem says it expresses "equality of $d_+ = \dim \operatorname{Ran}(A+i)^\perp$ and $d_- = \dim \operatorname{Ran}(A-i)^\perp$ … as the existence of a unitary between the two defect spaces." That is a comment, not code, and I cannot confirm from the code alone that the predicate says this.

The equivalence runs both ways. If some self-adjoint extension of $A$ exists, then $A$ has equal defect indices. Conversely, if $A$ has equal defect indices, a self-adjoint extension exists. The extension $B$ may be $A$ itself, and nothing is said about how many such extensions there are.

Degenerate cases.

$H = \{0\}$ : there is exactly one partially defined operator, with domain $\{0\}$ and value $0$ . It equals its own adjoint, so the left-hand side holds with $B = A$ . The statement then asserts that $\mathrm{HasEqualDefectIndices}(A)$ holds as well. Whether that is true depends on the unseen definition; for example, a unitary between two zero spaces exists trivially.
Non-dense domain: if $\mathrm{IsSymmetric}$ does not require $\mathfrak{D}(A)$ to be dense, the hypothesis allows non-densely defined $A$ . For such $A$ , the library's convention (the adjoint is zero on non-dense domains) affects which operators $B$ count as self-adjoint only through $B$ itself. When $H \ne \{0\}$ , any qualifying $B$ must be densely defined.
Unsatisfiable or trivially true predicates: if either $\mathrm{IsSymmetric}$ or $\mathrm{HasEqualDefectIndices}$ is defined so that it can never hold, or always holds, the equivalence inherits that. I cannot tell which from the code shown.
No finiteness condition: no dimension or cardinality assumption is placed on the defect spaces. The statement covers infinite defect indices on the same footing as finite ones.

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph