Theorem 2.26, (2.103)–(2.104) — domain and action of a self-adjoint extension

Proved

TeschlQM.SelfAdjoint.selfAdjoint_extension_domain

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

cayley-transformextensionsfunctional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1self-adjoint-operators

Let $A$ be a closed symmetric operator on a complex Hilbert space, let $A_1$ be a self-adjoint extension of $A$ and let $V_1$ be the Cayley transform of $A_1$ . With $K_+ = \operatorname{Ran}(A + \mathrm{i})^\perp$ ,

\mathfrak{D}(A_1) = \mathfrak{D}(A) + (1 - V_1)K_+ = \{\psi + \varphi_+ - V_1\varphi_+ \mid \psi \in \mathfrak{D}(A),\ \varphi_+ \in K_+\}

and

A_1(\psi + \varphi_+ - V_1\varphi_+) = A\psi + \mathrm{i}\varphi_+ + \mathrm{i}V_1\varphi_+.

Formalization Note. The hypothesis that $A$ is closed is added. The book states (2.103) for every symmetric $A$ , but for a non-closed one it fails: if $A$ is essentially self-adjoint and not closed, then $K_+ = \{0\}$ and $\mathfrak{D}(A_1) = \mathfrak{D}(\overline{A}) \ne \mathfrak{D}(A)$ . The book's proof uses $\mathfrak{H} = \operatorname{Ran}(A+\mathrm{i}) \oplus K_+$ , which holds exactly when $\operatorname{Ran}(A + \mathrm{i})$ is closed (Lemma 2.27). Since $A_1$ is self-adjoint, $\mathfrak{D}(V_1) = \mathfrak{H}$ , so letting $\varphi_+$ range over $\mathfrak{D}(V_1) \cap K_+$ is the same as letting it range over $K_+$ .

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_IsSymmetric
import Definitions.Def_TeschlQM_SelfAdjoint_IsCayleyTransform
import Definitions.Def_TeschlQM_SelfAdjoint_defectSpace

Formal statement

namespace TeschlQM.SelfAdjoint

/-- Teschl, Theorem 2.26, (2.103)–(2.104) (p. 82): let `A₁` be a self-adjoint extension of the
symmetric operator `A` and `V₁` its Cayley transform. Then
`𝔇(A₁) = {ψ + φ₊ - V₁φ₊ | ψ ∈ 𝔇(A), φ₊ ∈ K₊}` and `A₁(ψ + φ₊ - V₁φ₊) = Aψ + iφ₊ + iV₁φ₊`.
The hypothesis that `A` is closed is added: without it (2.103) fails (for an essentially
self-adjoint, non-closed `A`, `K₊ = {0}` and `𝔇(A₁) = 𝔇(Ā) ≠ 𝔇(A)`). `𝔇(V₁) = ℌ` since `A₁` is
self-adjoint, so quantifying `φ₊` over `𝔇(V₁) ∩ K₊` is quantifying over `K₊`. -/
theorem selfAdjoint_extension_domain {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (A A₁ V₁ : H →ₗ.[ℂ] H) (hA : TeschlQM.Shared.IsSymmetric A) (hAc : A.IsClosed)
    (hA₁ : IsSelfAdjoint A₁) (hAA₁ : A ≤ A₁) (hV₁ : IsCayleyTransform A₁ V₁) :
    (A₁.domain : Set H) =
        {x : H | ∃ ψ : A.domain, ∃ φ : V₁.domain, (φ : H) ∈ defectPlus A ∧
          x = (ψ : H) + (φ : H) - V₁ φ} ∧
      ∀ (ψ : A.domain) (φ : V₁.domain), (φ : H) ∈ defectPlus A →
        ∀ h : (ψ : H) + (φ : H) - V₁ φ ∈ A₁.domain,
          A₁ ⟨(ψ : H) + (φ : H) - V₁ φ, h⟩ = A ψ + Complex.I • (φ : H) + Complex.I • V₁ φ := by sorry

end TeschlQM.SelfAdjoint

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 82, Theorem 2.26, Eqs. (2.103)–(2.104)

Read-back

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

Let $H$ be a complex Hilbert space: a complete complex inner product space. Let $A$ , $A_1$ and $V_1$ be partial $\mathbb C$ -linear operators on $H$ , with domains $\mathcal D(A)$ , $\mathcal D(A_1)$ and $\mathcal D(V_1)$ . Assume:

$\mathrm{IsSymmetric}(A)$ holds. This predicate is imported and its code is not shown.
$A$ is closed: its graph is closed in $H\times H$ .
$A_1$ is self-adjoint: $A_1=A_1^*$ , with equal domains and values. $A_1^*$ is the usual adjoint when $\mathcal D(A_1)$ is dense, and the zero operator on all of $H$ otherwise.
$A\le A_1$ : that is, $\mathcal D(A)\subseteq\mathcal D(A_1)$ and $A_1\psi=A\psi$ for $\psi\in\mathcal D(A)$ .
$\mathrm{IsCayleyTransform}(A_1,V_1)$ holds. This predicate is imported and its code is not shown.

Let $K_+(A)$ denote the imported subspace $\operatorname{defectPlus}(A)$ , whose code is not shown.

Conclusion. Both of the following hold.

Domain formula.

\mathcal D(A_1)=\{\,\psi+\varphi-V_1\varphi\;:\;\psi\in\mathcal D(A),\ \varphi\in\mathcal D(V_1),\ \varphi\in K_+(A)\,\}.

The $\varphi$ range only over $\mathcal D(V_1)\cap K_+(A)$ .

Action formula. For every $\psi\in\mathcal D(A)$ and every $\varphi\in\mathcal D(V_1)\cap K_+(A)$ such that $\psi+\varphi-V_1\varphi\in\mathcal D(A_1)$ :

A_1(\psi+\varphi-V_1\varphi)=A\psi+i\varphi+i\,V_1\varphi.

Degenerate cases:

If $H=\{0\}$ , every term is $0$ and both formulas hold trivially.
If $\mathcal D(V_1)\cap K_+(A)=\{0\}$ , the domain formula asserts $\mathcal D(A_1)=\mathcal D(A)$ , and the action formula reduces to $A_1\psi=A\psi$ .
If $\mathcal D(A_1)$ is not dense, $A_1$ cannot equal $A_1^*$ , so no such $A_1$ exists.

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