Theorem 2.19 — inf σ(A) and sup σ(A) as extremes of ⟨ψ, Aψ⟩ over unit vectors

Proved

TeschlQM.MinMax.inf_sup_spectrum

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

functional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1self-adjoint-operatorsspectral-theoryvariational-methods

Let $A$ be a self-adjoint operator on a complex Hilbert space $\mathfrak H$ with domain $\mathfrak D(A)$ and spectrum $\sigma(A) \subseteq \mathbb R$ . Then

\inf \sigma(A) = \inf_{\psi \in \mathfrak D(A),\ \|\psi\| = 1} \langle \psi, A\psi \rangle \qquad\text{and}\qquad \sup \sigma(A) = \sup_{\psi \in \mathfrak D(A),\ \|\psi\| = 1} \langle \psi, A\psi \rangle .

The bottom of the spectrum is thus the infimum of the expectation values of $A$ ; it is the case $n = 1$ of the min-max principle and the reason why any normalized trial vector gives an upper bound for the lowest eigenvalue.

Formalization Note. Both sides are in the extended reals EReal, so either side may be $\pm\infty$ (for an operator unbounded below or above; for $\mathfrak H = \{0\}$ both infima are $+\infty$ and both suprema $-\infty$ ). Since the spectrum of a self-adjoint operator is real, $\sigma(A)$ enters as the set of real $x$ with $x \in \sigma(A)$ , the resolvent spectrum of p. 73; $\langle\psi, A\psi\rangle$ enters through its real part. The operator is a LinearPMap and self-adjointness is Mathlib's IsSelfAdjoint, which includes a dense domain.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_MinMax_spectrum

open scoped InnerProductSpace

Formal statement

namespace TeschlQM.MinMax

/-- Teschl, Theorem 2.19, p. 77, (2.90) and (2.91): for a self-adjoint `A`,
`inf σ(A) = inf_{ψ ∈ 𝔇(A), ‖ψ‖ = 1} ⟨ψ, Aψ⟩` and `sup σ(A) = sup_{ψ ∈ 𝔇(A), ‖ψ‖ = 1} ⟨ψ, Aψ⟩`,
in `EReal` (either side may be `±∞`; both are `+∞`/`−∞` when `ℌ = {0}`).
The spectrum of a self-adjoint operator is real, so `σ(A)` is taken as the set of real `x`
with `x ∈ σ(A)`. -/
theorem inf_sup_spectrum {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] (A : H →ₗ.[ℂ] H) (hA : IsSelfAdjoint A) :
    sInf ((fun x : ℝ => (x : EReal)) '' {x : ℝ | (x : ℂ) ∈ spectrum A}) =
        ⨅ (ψ : A.domain) (_ : ‖(ψ : H)‖ = 1), ((⟪(ψ : H), A ψ⟫_ℂ).re : EReal) ∧
      sSup ((fun x : ℝ => (x : EReal)) '' {x : ℝ | (x : ℂ) ∈ spectrum A}) =
        ⨆ (ψ : A.domain) (_ : ‖(ψ : H)‖ = 1), ((⟪(ψ : H), A ψ⟫_ℂ).re : EReal) := by sorry

end TeschlQM.MinMax

Source

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

Read-back

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

This theorem is stated for a complex Hilbert space $\mathcal H$ and a linear operator $A$ with domain $\mathcal D(A)\subseteq\mathcal H$ . The only hypothesis is that $A$ is self-adjoint in Mathlib's sense: $A$ equals its adjoint $A^*$ , with the same domain and the same values. $\sigma(A)$ denotes the imported spectrum, a subset of $\mathbb C$ , whose body is not part of this declaration's text. Let

S = \{x\in\mathbb R : x\in\sigma(A)\},

the real points of $\sigma(A)$ . The inner product is conjugate-linear in its first argument.

The theorem asserts both of the following equalities, in the extended reals $[-\infty,+\infty]$ :

\inf S = \inf_{\substack{\psi\in\mathcal D(A)\\ \|\psi\|=1}} \operatorname{Re}\langle\psi, A\psi\rangle \qquad\text{and}\qquad \sup S = \sup_{\substack{\psi\in\mathcal D(A)\\ \|\psi\|=1}} \operatorname{Re}\langle\psi, A\psi\rangle .

Only the real part of $\langle\psi,A\psi\rangle$ enters, and only the real points of $\sigma(A)$ enter.

Degenerate cases.

Infinite values. Either side may be $\pm\infty$ ; the claim then equates those extended-real values.
$\mathcal H=\{0\}$ . There are no unit vectors, so the right-hand sides are $+\infty$ (infimum) and $-\infty$ (supremum). The statement then asserts $\inf S=+\infty$ and $\sup S=-\infty$ , i.e. that $\sigma(A)$ contains no real point.

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