Lemma 2.7 — criterion for essential self-adjointness

Proved

TeschlQM.SelfAdjoint.essentiallySelfAdjoint_iff

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

essential-self-adjointnessfunctional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1self-adjoint-operators

Let $A$ be a symmetric operator on a complex Hilbert space $\mathfrak{H}$ . Then $A$ is essentially self-adjoint if and only if one of the following conditions holds for one $z \in \mathbb{C}\setminus\mathbb{R}$ :

\overline{\operatorname{Ran}(A + z)} = \overline{\operatorname{Ran}(A + z^*)} = \mathfrak{H}, \qquad\text{or}\qquad \operatorname{Ker}(A^* + z) = \operatorname{Ker}(A^* + z^*) = \{0\}.

If $A$ is nonnegative, that is $\langle \psi, A\psi\rangle \ge 0$ for all $\psi \in \mathfrak{D}(A)$ , then real $z$ may also be admitted, namely $z > 0$ (so that the spectral parameter $-z$ of $A + z = A - (-z)$ lies in $(-\infty, 0)$ ).

Formalization Note. Each of the two conditions is stated separately as equivalent to essential self-adjointness, each with an existential "for one $z$ ". The closure of the range is Submodule.topologicalClosure; $A^*$ is Mathlib's LinearPMap.adjoint, which is the book's adjoint because symmetric operators are densely defined. Nonnegativity is $\operatorname{Re}\langle\psi, A\psi\rangle \ge 0$ (the form is real for symmetric $A$ ), and the admitted $z$ are then those with $\operatorname{Im} z \ne 0$ or with $z$ real and positive. The book writes " $z \in (-\infty, 0)$ " with the conditions on $A + z$ ; read literally that is false ( $A = -d^2/dx^2$ on $C_c^\infty(0,\infty)$ is nonnegative and not essentially self-adjoint, while $\operatorname{Ker}(A^* - 1) = \{0\}$ ). The book's proof uses $A + \varepsilon$ with $\varepsilon > 0$ , which is the version stated here.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_IsSymmetric
import Definitions.Def_TeschlQM_SelfAdjoint_addScalar
import Definitions.Def_TeschlQM_Shared_IsEssentiallySelfAdjoint

Formal statement

namespace TeschlQM.SelfAdjoint

open ComplexConjugate
open scoped InnerProductSpace

/-- Teschl, Lemma 2.7 (p. 66): a symmetric `A` is essentially self-adjoint iff, for one
`z ∈ ℂ \ ℝ`, `closure(Ran(A + z)) = closure(Ran(A + z*)) = ℌ`, iff, for one `z ∈ ℂ \ ℝ`,
`Ker(A* + z) = Ker(A* + z*) = {0}`. If `A` is nonnegative (`⟨ψ, Aψ⟩ ≥ 0` on `𝔇(A)`), real `z`
may also be admitted. The book writes `z ∈ (-∞, 0)`, but its conditions are on `A + z` and its proof
uses `A + ε` with `ε > 0`; read literally the clause is false (`-d²/dx²` on `C_c^∞(0, ∞)` is
nonnegative, not essentially self-adjoint, and `Ker(A* - 1) = {0}`), so the admitted real `z` are
`z ∈ (0, ∞)` in the `A + z` convention, i.e. the spectral point `-z ∈ (-∞, 0)`. -/
theorem essentiallySelfAdjoint_iff {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (A : H →ₗ.[ℂ] H) (hA : TeschlQM.Shared.IsSymmetric A) :
    (TeschlQM.Shared.IsEssentiallySelfAdjoint A ↔
      ∃ z : ℂ, z.im ≠ 0 ∧ (rangeAdd A z).topologicalClosure = ⊤ ∧
        (rangeAdd A (conj z)).topologicalClosure = ⊤) ∧
    (TeschlQM.Shared.IsEssentiallySelfAdjoint A ↔
      ∃ z : ℂ, z.im ≠ 0 ∧ kerAdd A.adjoint z = ⊥ ∧ kerAdd A.adjoint (conj z) = ⊥) ∧
    ((∀ ψ : A.domain, 0 ≤ (⟪(ψ : H), A ψ⟫_ℂ).re) →
      (TeschlQM.Shared.IsEssentiallySelfAdjoint A ↔
        ∃ z : ℂ, (z.im ≠ 0 ∨ (z.im = 0 ∧ 0 < z.re)) ∧ (rangeAdd A z).topologicalClosure = ⊤ ∧
          (rangeAdd A (conj z)).topologicalClosure = ⊤) ∧
      (TeschlQM.Shared.IsEssentiallySelfAdjoint A ↔
        ∃ z : ℂ, (z.im ≠ 0 ∨ (z.im = 0 ∧ 0 < z.re)) ∧ kerAdd A.adjoint z = ⊥ ∧
          kerAdd A.adjoint (conj z) = ⊥)) := by sorry

end TeschlQM.SelfAdjoint

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 66, Lemma 2.7

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. $\langle x,y\rangle$ is conjugate-linear in $x$ . Let $A$ be a partial $\mathbb C$ -linear operator on $H$ with domain $\mathcal D(A)$ , and assume $\mathrm{IsSymmetric}(A)$ .

The statement uses the following notation:

$\mathrm{ESA}(A)$ denotes the imported predicate IsEssentiallySelfAdjoint.
$\operatorname{rangeAdd}(\cdot,\cdot)$ and $\operatorname{kerAdd}(\cdot,\cdot)$ are imported subspace-valued definitions.
The predicates $\mathrm{IsSymmetric}$ and $\mathrm{ESA}$ , like these two subspaces, have code that is not shown here.
$A^*$ is the adjoint. When $\mathcal D(A)$ is dense, it is the usual adjoint: $y\in\mathcal D(A^*)$ iff $\psi\mapsto\langle y,A\psi\rangle$ is continuous on $\mathcal D(A)$ , and then $\langle A^*y,\psi\rangle=\langle y,A\psi\rangle$ . When $\mathcal D(A)$ is not dense, $A^*$ is the zero operator on all of $H$ .
$\overline{S}$ denotes the topological closure of a subspace $S$ .

The statement is a conjunction of three parts.

$\mathrm{ESA}(A)$ holds if and only if there exists $z\in\mathbb C$ with $\operatorname{Im}z\neq0$ such that

\overline{\operatorname{rangeAdd}(A,z)}=H\quad\text{and}\quad\overline{\operatorname{rangeAdd}(A,\bar z)}=H.

$\mathrm{ESA}(A)$ holds if and only if there exists $z\in\mathbb C$ with $\operatorname{Im}z\neq0$ such that

\operatorname{kerAdd}(A^*,z)=\{0\}\quad\text{and}\quad\operatorname{kerAdd}(A^*,\bar z)=\{0\}.

Suppose $\operatorname{Re}\langle\psi,A\psi\rangle\ge0$ for every $\psi\in\mathcal D(A)$ . Only the real part is constrained. Then both of the following hold:
- $\mathrm{ESA}(A)$ holds if and only if there exists $z$ with $\operatorname{Im}z\neq0$ , or with $\operatorname{Im}z=0$ and $\operatorname{Re}z>0$ , such that $\overline{\operatorname{rangeAdd}(A,z)}=\overline{\operatorname{rangeAdd}(A,\bar z)}=H$ ;
- $\mathrm{ESA}(A)$ holds if and only if there exists $z$ satisfying the same condition on $z$ , such that $\operatorname{kerAdd}(A^*,z)=\operatorname{kerAdd}(A^*,\bar z)=\{0\}$ .
The admitted real values of $z$ are exactly the strictly positive reals. $z=0$ and negative reals are excluded.

In each part, the right-hand side is existential: a single suitable $z$ is enough.

Degenerate cases:

For real $z>0$ in part 3, $\bar z=z$ , so each pair of conditions collapses to one condition.
If $H=\{0\}$ , every closure equals $H$ and every kernel is $\{0\}$ whatever the imported definitions give. So every right-hand side holds, and the statement asserts $\mathrm{ESA}(A)$ .
If $\mathcal D(A)$ is not dense, then $A^*$ is the zero operator on $H$ . The kernel conditions then concern $\operatorname{kerAdd}$ of that zero operator.
Whether the nonnegativity hypothesis or IsSymmetric can be satisfied in a given case depends on the unseen imported definitions.

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