Theorem 4.13 — Temple's inequality

Proved

TeschlQM.MinMax.temple

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

eigenvalue-boundsfunctional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1self-adjoint-operatorsspectral-theory

Let $A$ be a self-adjoint operator on a complex Hilbert space $\mathfrak H$ , let $\lambda_1 < \lambda_2$ , and let $\psi \in \mathfrak D(A)$ with $\|\psi\| = 1$ such that

\lambda = \langle \psi, A\psi \rangle \in (\lambda_1, \lambda_2).

If there is exactly one point $E$ of the spectrum between $\lambda_1$ and $\lambda_2$ , that is $\sigma(A) \cap (\lambda_1, \lambda_2) = \{E\}$ (then $E$ is an isolated eigenvalue), then

\lambda - \frac{\|(A - \lambda)\psi\|^2}{\lambda_2 - \lambda} \le E \le \lambda + \frac{\|(A - \lambda)\psi\|^2}{\lambda - \lambda_1}.

Together with the variational upper bound, Temple's inequality gives a computable two-sided enclosure of an isolated eigenvalue from a single trial vector and its residual.

Formalization Note. $\sigma(A)$ is the resolvent spectrum of p. 73, and $\sigma(A) \cap (\lambda_1, \lambda_2)$ is the set of real $x \in (\lambda_1, \lambda_2)$ with $x \in \sigma(A)$ . That $E$ is an eigenvalue is not assumed; it follows from the hypotheses. The hypothesis $\lambda = \langle\psi, A\psi\rangle$ is an equality of complex numbers.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_MinMax_spectrum

open scoped InnerProductSpace

Formal statement

namespace TeschlQM.MinMax

/-- Teschl, Theorem 4.13 (Temple's inequality), p. 120, (4.37)–(4.38): let `A` be self-adjoint,
`λ₁ < λ₂` and `ψ ∈ 𝔇(A)` with `‖ψ‖ = 1` such that `λ = ⟨ψ, Aψ⟩ ∈ (λ₁, λ₂)`. If
`σ(A) ∩ (λ₁, λ₂) = {E}` (one isolated eigenvalue `E` between `λ₁` and `λ₂`), then
`λ − ‖(A − λ)ψ‖²/(λ₂ − λ) ≤ E ≤ λ + ‖(A − λ)ψ‖²/(λ − λ₁)`. -/
theorem temple {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (A : H →ₗ.[ℂ] H) (hA : IsSelfAdjoint A) (lam₁ lam₂ : ℝ) (hlt : lam₁ < lam₂)
    (ψ : A.domain) (hψ : ‖(ψ : H)‖ = 1) (lam : ℝ) (hlam : ⟪(ψ : H), A ψ⟫_ℂ = (lam : ℂ))
    (hmem : lam ∈ Set.Ioo lam₁ lam₂) (E : ℝ)
    (hE : {x : ℝ | (x : ℂ) ∈ spectrum A} ∩ Set.Ioo lam₁ lam₂ = {E}) :
    lam - ‖A ψ - (lam : ℂ) • (ψ : H)‖ ^ 2 / (lam₂ - lam) ≤ E ∧
      E ≤ lam + ‖A ψ - (lam : ℂ) • (ψ : H)‖ ^ 2 / (lam - lam₁) := by sorry

end TeschlQM.MinMax

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 120, Theorem 4.13

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$ is a self-adjoint linear operator (Mathlib's sense) with domain $\mathcal D(A)$ .
$\lambda_1<\lambda_2$ are real numbers.
$\psi\in\mathcal D(A)$ with $\|\psi\|=1$ .
$\lambda$ is a real number with $\langle\psi,A\psi\rangle=\lambda$ as complex numbers. So this inner product is real and equals $\lambda$ .
$\lambda_1<\lambda<\lambda_2$ .
$E$ is a real number such that

\{x\in\mathbb R : x\in\sigma(A)\}\cap(\lambda_1,\lambda_2)=\{E\}.

Here $\sigma(A)$ is the imported spectrum, not unfolded here. In words, $E$ is the only real point of $\sigma(A)$ in the open interval.

The conclusion is the pair of inequalities

\lambda-\frac{\|A\psi-\lambda\psi\|^2}{\lambda_2-\lambda}\ \le\ E\ \le\ \lambda+\frac{\|A\psi-\lambda\psi\|^2}{\lambda-\lambda_1}.

The hypotheses do not say that $E$ is an eigenvalue, and they say nothing about whether $\lambda_1$ or $\lambda_2$ themselves lie in $\sigma(A)$ .

Degenerate cases.

Division by zero. Both denominators $\lambda_2-\lambda$ and $\lambda-\lambda_1$ are strictly positive under the hypotheses, so no division-by-zero default arises.
$\mathcal H=\{0\}$ . Excluded, because $\|\psi\|=1$ is required.
$A\psi=\lambda\psi$ . The statement then asserts $E=\lambda$ .
Hypotheses that cannot hold. If $\sigma(A)$ has no real point or several real points in $(\lambda_1,\lambda_2)$ , the hypothesis on $E$ cannot be satisfied and the theorem says nothing.

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