Corollary 4.11 — A ≥ B implies Eₙ(A) ≥ Eₙ(B)

Proved

TeschlQM.MinMax.eigenvalueSeq_mono

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$ and $B$ be self-adjoint operators on a complex Hilbert space $\mathfrak H$ with $A \ge B$ , i.e. $A - B \ge 0$ , where $\mathfrak D(A) \subseteq \mathfrak D(B)$ and

\langle \psi, (A - B)\psi \rangle \ge 0 \qquad \text{for all } \psi \in \mathfrak D(A - B) = \mathfrak D(A).

Then for every $n \ge 1$ ,

E_n(A) \ge E_n(B),

where $E_n(\cdot)$ are the eigenvalues below the essential spectrum counted with multiplicity, respectively the infimum of the essential spectrum, as in the min-max principle.

Increasing an operator can only raise each of these eigenvalues.

Formalization Note. The book writes only " $A - B \ge 0$ ". Read literally on $\mathfrak D(A) \cap \mathfrak D(B)$ the statement would be false (that intersection can be $\{0\}$ ), so the operator $A - B$ is taken with domain $\mathfrak D(A)$ , i.e. the hypothesis $\mathfrak D(A) \subseteq \mathfrak D(B)$ is stated, which is the reading under which the corollary follows from (4.32). $E_n$ is eigenvalueSeq (values in EReal).

Preamble

import Mathlib
import Definitions.Def_TeschlQM_MinMax_eigenvalueSeq

open scoped InnerProductSpace

Formal statement

namespace TeschlQM.MinMax

/-- Teschl, Corollary 4.11, p. 119: if `A` and `B` are self-adjoint with `A ≥ B`, i.e.
`A − B ≥ 0`, then `E_n(A) ≥ E_n(B)` for every `n ≥ 1`. Here `A − B ≥ 0` is read with
`𝔇(A − B) = 𝔇(A) ∩ 𝔇(B) = 𝔇(A)`: `𝔇(A) ⊆ 𝔇(B)` and `⟨ψ, (A − B)ψ⟩ ≥ 0` for `ψ ∈ 𝔇(A)`. -/
theorem eigenvalueSeq_mono {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] (A B : H →ₗ.[ℂ] H) (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint B)
    (hdom : A.domain ≤ B.domain)
    (hAB : ∀ (ψ : H) (hψA : ψ ∈ A.domain) (hψB : ψ ∈ B.domain),
      0 ≤ (⟪ψ, A ⟨ψ, hψA⟩ - B ⟨ψ, hψB⟩⟫_ℂ).re)
    (n : ℕ) (hn : 1 ≤ n) :
    eigenvalueSeq B n ≤ eigenvalueSeq A n := by sorry

end TeschlQM.MinMax

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 119, Corollary 4.11

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$ . It has the following hypotheses:

$A$ and $B$ are self-adjoint (Mathlib's sense) linear operators with domains $\mathcal D(A)$ and $\mathcal D(B)$ .
$\mathcal D(A)\subseteq\mathcal D(B)$ .
For every $\psi$ lying in both $\mathcal D(A)$ and $\mathcal D(B)$ (which, given the inclusion, means every $\psi\in\mathcal D(A)$ ):

\operatorname{Re}\langle\psi, A\psi - B\psi\rangle\ge 0 .

$n\in\mathbb N$ with $n\ge1$ .

The conclusion is the extended-real inequality

E_n(B)\le E_n(A),

where $E_n(\cdot)\in[-\infty,+\infty]$ is the imported eigenvalueSeq. Its body is not part of this declaration's text and is not unfolded here.

Degenerate cases.

$n=0$ . Excluded by the hypothesis $n\ge1$ .
Infinite values. Either side may be $\pm\infty$ ; the inequality is then read in the extended reals.
$\mathcal H=\{0\}$ . The form hypothesis holds trivially, and the claim reduces to $E_n(B)\le E_n(A)$ for two operators on the zero space.

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