Theorem 4.10 — the min-max principle

Proved

TeschlQM.MinMax.min_max

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 let $E_1 \le E_2 \le E_3 \le \cdots$ be the eigenvalues of $A$ below the essential spectrum, counted according to their multiplicity, respectively the infimum of the essential spectrum once there are no more eigenvalues left. For $\psi_1, \dots, \psi_{n-1} \in \mathfrak H$ let

U(\psi_1, \dots, \psi_{n-1}) = \{ \psi \in \mathfrak D(A) \mid \|\psi\| = 1,\ \psi \in \operatorname{span}\{\psi_1, \dots, \psi_{n-1}\}^\perp \}.

Then for every $n \ge 1$

E_n = \sup_{\psi_1, \dots, \psi_{n-1}} \ \inf_{\psi \in U(\psi_1, \dots, \psi_{n-1})} \langle \psi, A\psi \rangle ,

where the supremum runs over all $(n-1)$ -tuples of vectors of $\mathfrak H$ .

The min-max principle characterizes the eigenvalues below the essential spectrum without knowing the eigenvectors, and is the basis of the Rayleigh–Ritz method for bounding them.

Formalization Note. $E_n$ is eigenvalueSeq A n, defined from the spectrum, the essential spectrum $\sigma_{ess}(A) = \sigma(A) \setminus \sigma_d(A)$ of p. 145 and the dimensions of eigenspaces (cardinals), not from the min-max expression. All values are in EReal: the infimum over an empty $U$ is $+\infty$ and the equality also covers the cases the book leaves implicit ( $A$ unbounded below, where both sides are $-\infty$ ; $\sigma_{ess}(A) = \emptyset$ with fewer than $n$ eigenvalues, where both sides are $+\infty$ ). $\langle\psi, A\psi\rangle$ enters through its real part. For $n = 1$ the tuple is empty and $U$ is the unit sphere of $\mathfrak D(A)$ . No projection-valued measure is used, and the Hilbert space is not assumed separable.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_MinMax_eigenvalueSeq
import Definitions.Def_TeschlQM_MinMax_minMaxSet

open scoped InnerProductSpace

Formal statement

namespace TeschlQM.MinMax

/-- Teschl, Theorem 4.10 (Min-max), p. 119, (4.32): let `A` be self-adjoint and let
`E₁ ≤ E₂ ≤ E₃ ≤ ⋯` be the eigenvalues of `A` below the essential spectrum (counted with
multiplicity), respectively `inf σ_ess(A)` once there are no more eigenvalues left
(`eigenvalueSeq A n`). Then for every `n ≥ 1`
`E_n = sup_{ψ₁, …, ψ_{n−1} ∈ ℌ} inf_{ψ ∈ U(ψ₁, …, ψ_{n−1})} ⟨ψ, Aψ⟩`, with `U` as in (4.28).
Values are in `EReal`; an infimum over an empty `U` is `+∞`. -/
theorem min_max {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (A : H →ₗ.[ℂ] H) (hA : IsSelfAdjoint A) (n : ℕ) (hn : 1 ≤ n) :
    eigenvalueSeq A n =
      ⨆ ψ : Fin (n - 1) → H, ⨅ φ ∈ minMaxSet A ψ, ((⟪(φ : H), A φ⟫_ℂ).re : EReal) := by sorry

end TeschlQM.MinMax

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 119, Theorem 4.10

Read-back

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

Let $\mathcal H$ be a complex Hilbert space: a normed additive group with a $\mathbb C$ -inner product that makes it complete. No separability is assumed, and $\mathcal H$ may be the trivial space $\{0\}$ . The inner product $\langle \cdot,\cdot\rangle$ follows Mathlib's convention: conjugate-linear in the first argument and linear in the second. Let $A$ be a possibly unbounded partially defined $\mathbb C$ -linear operator on $\mathcal H$ . It is a linear map defined on a subspace $\mathcal D(A)\subseteq\mathcal H$ (its domain), and nothing is assumed about that domain in advance. The hypothesis $\mathrm{hA}$ says $A$ is self-adjoint in Mathlib's sense for partial linear maps: $A$ equals its adjoint $A^{*}$ , with the same domain and the same values. In Mathlib the adjoint of an operator whose domain is not dense is a conventional default (the zero map on the adjoint's domain), not the usual adjoint. Finally, let $n$ be a natural number with $n\ge 1$ .

The statement uses two objects defined in imported files whose contents are not shown here. From how they are used here, this much can be said:

$E_n := \mathrm{eigenvalueSeq}(A,n)$ is an extended real number, in $[-\infty,+\infty]$ , that depends on $A$ and $n$ .
For a tuple $\psi=(\psi_1,\dots,\psi_{n-1})$ of vectors of $\mathcal H$ , $U_A(\psi) := \mathrm{minMaxSet}(A,\psi)$ is a set of elements of the domain $\mathcal D(A)$ . This follows because $A$ is applied to its members.

The accompanying comment describes $E_n$ as "the $n$ -th eigenvalue below the essential spectrum, counted with multiplicity, or $\inf\sigma_{\mathrm{ess}}(A)$ when there are no more". It also says $U$ is "the set of (4.28)". Those descriptions are the author's comments. Whether the imported definitions actually encode them cannot be checked from this code. In particular, it is not visible whether $U_A(\psi)$ is restricted to unit vectors or to vectors orthogonal to $\psi_1,\dots,\psi_{n-1}$ .

The theorem asserts the equality of extended reals

E_n \;=\; \sup_{\psi\in\mathcal H^{\,n-1}}\ \inf_{\varphi\in U_A(\psi)}\ \operatorname{Re}\langle \varphi, A\varphi\rangle .

The supremum ranges over all $(n-1)$ -tuples $(\psi_1,\dots,\psi_{n-1})$ of arbitrary vectors of $\mathcal H$ . They need not be in $\mathcal D(A)$ , and they need not be nonzero, normalized, orthogonal or distinct.
The inner quantity is the real part of $\langle\varphi,A\varphi\rangle$ , viewed as an extended real number.
Both the supremum and the infimum are taken in the complete lattice $[-\infty,+\infty]$ , so each always exists and may be $\pm\infty$ .

Degenerate cases:

$n = 1$ . Because $n\ge1$ , the natural-number subtraction $n-1$ is never truncated. For $n=1$ there are no $\psi$ 's: the supremum runs over the single empty tuple, so the claim is $E_1=\inf_{\varphi\in U_A(())}\operatorname{Re}\langle\varphi,A\varphi\rangle$ .
The supremum. Its index set is never empty, since the tuple of zero vectors always exists. So it is never $\sup\emptyset=-\infty$ . It is $+\infty$ if the inner infima are unbounded above or if some $U_A(\psi)$ is empty.
Empty $U_A(\psi)$ . For any tuple $\psi$ with $U_A(\psi)=\emptyset$ , the inner infimum is $\inf\emptyset=+\infty$ . If that happens for some $\psi$ , the right-hand side is $+\infty$ and the theorem asserts $E_n=+\infty$ .
Unbounded below. If the values $\operatorname{Re}\langle\varphi,A\varphi\rangle$ over $U_A(\psi)$ are unbounded below, that inner infimum is $-\infty$ .
Trivial space. If $\mathcal H=\{0\}$ , then $\mathcal D(A)=\{0\}$ and every quadratic form value is $\operatorname{Re}\langle0,A0\rangle=0$ . So every inner infimum is $0$ if $U_A(\psi)$ contains $0$ and $+\infty$ if it is empty. The claim then pins $E_n$ to $0$ or $+\infty$ , depending on the unseen definition of $\mathrm{minMaxSet}$ . (Only the zero tuple exists in this case, so the supremum has a single term.)
Non-dense domain. If $\mathcal D(A)$ is not dense, the self-adjointness hypothesis refers to Mathlib's default adjoint described above rather than the classical one.

No boundedness, semiboundedness, compactness or discrete-spectrum assumption is made on $A$ . The statement is claimed for every $n\ge1$ .

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