Theorem 2.18 — self-adjoint iff σ(A) ⊆ ℝ; resolvent bounds

Proved

TeschlQM.SelfAdjoint.selfAdjoint_iff_spectrum_real

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

functional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1resolventself-adjoint-operatorsspectral-theory

Let $A$ be a symmetric operator on a complex Hilbert space $\mathfrak{H}$ and $E \in \mathbb{R}$ . Then

$A$ is self-adjoint if and only if $\sigma(A) \subseteq \mathbb{R}$ ;
$A$ is self-adjoint with $A - E \ge 0$ if and only if $\sigma(A) \subseteq [E, \infty)$ ;
if $A$ is self-adjoint, then for $z \in \mathbb{C}\setminus\mathbb{R}$

\|R_A(z)\| \le |\operatorname{Im}(z)|^{-1};

if $A$ is self-adjoint and $A - E \ge 0$ , then $\|R_A(\lambda)\| \le |\lambda - E|^{-1}$ for real $\lambda < E$ .

Here $A - E \ge 0$ means $\langle \psi, (A - E)\psi \rangle \ge 0$ for all $\psi \in \mathfrak{D}(A)$ , and $\sigma(A)$ , $R_A(z)$ are the spectrum and resolvent of Section 2.4.

Formalization Note. $\sigma(A)$ is opSpectrum A, the complement of the set of $z$ for which $A - z$ has a bounded everywhere-defined two-sided inverse (not Mathlib's Banach-algebra spectrum). $A - E \ge 0$ is written $E\|\psi\|^2 \le \operatorname{Re}\langle\psi, A\psi\rangle$ . The norm bounds quantify over every bounded $R$ that is the resolvent at the given point; by parts 1–2 such an $R$ exists, and it is unique.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_IsSymmetric
import Definitions.Def_TeschlQM_Shared_resolventSet

Formal statement

namespace TeschlQM.SelfAdjoint

open scoped InnerProductSpace

/-- Teschl, Theorem 2.18 (p. 77): for symmetric `A`,
(i) `A` is self-adjoint iff `σ(A) ⊆ ℝ`;
(ii) for `E ∈ ℝ`, `A` is self-adjoint with `A - E ≥ 0` iff `σ(A) ⊆ [E, ∞)`;
(iii) for self-adjoint `A` and `z ∉ ℝ`, `‖R_A(z)‖ ≤ |Im z|⁻¹`;
(iv) for self-adjoint `A` with `A - E ≥ 0` and real `λ < E`, `‖R_A(λ)‖ ≤ |λ - E|⁻¹`.
`A - E ≥ 0` means `E‖ψ‖² ≤ Re⟨ψ, Aψ⟩` for `ψ ∈ 𝔇(A)` (the form is real for symmetric `A`). -/
theorem selfAdjoint_iff_spectrum_real {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (A : H →ₗ.[ℂ] H) (hA : TeschlQM.Shared.IsSymmetric A) :
    (IsSelfAdjoint A ↔ TeschlQM.Shared.spectrum A ⊆ {z : ℂ | z.im = 0}) ∧
    (∀ E : ℝ, (IsSelfAdjoint A ∧ ∀ ψ : A.domain, E * ‖(ψ : H)‖ ^ 2 ≤ (⟪(ψ : H), A ψ⟫_ℂ).re) ↔
      TeschlQM.Shared.spectrum A ⊆ {z : ℂ | z.im = 0 ∧ E ≤ z.re}) ∧
    (IsSelfAdjoint A → ∀ z : ℂ, z.im ≠ 0 → ∀ R : H →L[ℂ] H, TeschlQM.Shared.IsResolventAt A z R →
      ‖R‖ ≤ |z.im|⁻¹) ∧
    (∀ E : ℝ, IsSelfAdjoint A → (∀ ψ : A.domain, E * ‖(ψ : H)‖ ^ 2 ≤ (⟪(ψ : H), A ψ⟫_ℂ).re) →
      ∀ l : ℝ, l < E → ∀ R : H →L[ℂ] H, TeschlQM.Shared.IsResolventAt A (l : ℂ) R → ‖R‖ ≤ |l - E|⁻¹) := by sorry

end TeschlQM.SelfAdjoint

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 77, Theorem 2.18

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, with $\langle x,y\rangle$ 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:

$\sigma(A)\subseteq\mathbb C$ is the set given by the imported definition TeschlQM.Shared.spectrum.
$\mathrm{IsResolventAt}(A,z,R)$ is an imported predicate relating $A$ , a number $z\in\mathbb C$ and a bounded linear operator $R:H\to H$ .
$\|R\|$ is the operator norm.
IsSymmetric, spectrum and IsResolventAt are imported definitions whose code is not shown here.
Self-adjoint means $A=A^*$ , with equal domains and values. $A^*$ is the usual adjoint when $\mathcal D(A)$ is dense, and the zero operator on all of $H$ otherwise.
For a real number $E$ , write $\mathrm{LB}_E(A)$ for the condition that $E\|\psi\|^2\le\operatorname{Re}\langle\psi,A\psi\rangle$ for every $\psi\in\mathcal D(A)$ .

The statement is a conjunction of four parts.

$A$ is self-adjoint if and only if $\sigma(A)\subseteq\{z:\operatorname{Im}z=0\}$ .
For every real $E$ :

\big(A=A^*\ \text{and}\ \mathrm{LB}_E(A)\big)\iff \sigma(A)\subseteq\{z:\operatorname{Im}z=0,\ E\le\operatorname{Re}z\}.

Suppose $A$ is self-adjoint. Then for every $z$ with $\operatorname{Im}z\neq0$ , and every bounded $R$ with $\mathrm{IsResolventAt}(A,z,R)$ :

\|R\|\le\frac{1}{|\operatorname{Im}z|}.

Suppose $A$ is self-adjoint, $E$ is real and $\mathrm{LB}_E(A)$ holds. Then for every real $l<E$ , and every bounded $R$ with $\mathrm{IsResolventAt}(A,l,R)$ :

\|R\|\le\frac{1}{|l-E|}.

In parts 3 and 4, the bound applies to every $R$ satisfying the predicate. The statement does not assert that such an $R$ exists. If none exists, those parts hold vacuously.

Degenerate cases:

The reciprocals are never taken of zero: $\operatorname{Im}z\neq0$ in part 3, and $l<E$ in part 4.
If $H=\{0\}$ , then $\mathrm{LB}_E(A)$ holds for every $E$ . The content of parts 1 and 2 then depends on what the imported $\sigma(A)$ is for the zero operator on $\{0\}$ .
If $\mathcal D(A)$ is not dense, $A$ cannot equal $A^*$ . In that case part 1 asserts that $\sigma(A)$ is not contained in $\mathbb R$ .

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