Theorem 4.12 (ii) — ‖(A − (λ₂+λ₁)/2)ψ‖ < ((λ₂−λ₁)/2)‖ψ‖ on a k-dimensional span forces dim Ran P_A((λ₁, λ₂)) ≥ k

Proved

TeschlQM.MinMax.dim_range_ge_of_norm

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 projection-valued measure $P_A$ , let $\lambda_1 < \lambda_2$ , and let $\psi_1, \dots, \psi_k \in \mathfrak D(A)$ be linearly independent. If

\Big\| \Big(A - \frac{\lambda_2 + \lambda_1}{2}\Big)\psi \Big\| < \frac{\lambda_2 - \lambda_1}{2} \|\psi\|

for every nonzero linear combination $\psi = \sum_{j=1}^k c_j \psi_j$ , then

\dim \operatorname{Ran} P_A((\lambda_1, \lambda_2)) \ge k .

Approximate eigenvectors whose residual is small compared with the half-width of the interval thus certify spectral subspace of at least the corresponding dimension inside the interval.

Formalization Note. As in part (i), the projection-valued measure $P$ is taken as data with the hypothesis $A = \int \lambda\, dP(\lambda)$ , so $P_A = P$ . The vectors $\psi_j$ are elements of A.domain and the linear combinations are formed there. Dimensions are cardinals (Module.rank).

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_IsProjValuedMeasure
import Definitions.Def_TeschlQM_Shared_IsSpectralIntegral

Formal statement

namespace TeschlQM.MinMax

/-- Teschl, Theorem 4.12 (ii), p. 119, (4.35)–(4.36): let `A` be self-adjoint with
projection-valued measure `P` (i.e. `A = ∫ λ dP(λ)`, so `P_A = P`), let `λ₁ < λ₂` and let
`ψ₁, …, ψ_k ∈ 𝔇(A)` be linearly independent. If
`‖(A − (λ₂ + λ₁)/2)ψ‖ < ((λ₂ − λ₁)/2)‖ψ‖` for every nonzero linear combination `ψ` of the `ψ_j`,
then `dim Ran P_A((λ₁, λ₂)) ≥ k`. Dimensions are cardinals (`Module.rank`). -/
theorem dim_range_ge_of_norm {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] (A : H →ₗ.[ℂ] H) (hA : IsSelfAdjoint A)
    (P : Set ℝ → (H →L[ℂ] H)) (hP : TeschlQM.Shared.IsProjValuedMeasure P)
    (hAP : TeschlQM.Shared.IsSpectralIntegral P (fun x : ℝ => (x : ℂ)) A)
    (lam₁ lam₂ : ℝ) (hlt : lam₁ < lam₂)
    {k : ℕ} (ψ : Fin k → A.domain) (hli : LinearIndependent ℂ (fun j => (ψ j : H)))
    (h : ∀ φ ∈ Submodule.span ℂ (Set.range ψ), φ ≠ 0 →
      ‖A φ - (((lam₂ + lam₁) / 2 : ℝ) : ℂ) • (φ : H)‖ < (lam₂ - lam₁) / 2 * ‖(φ : H)‖) :
    (k : Cardinal) ≤ Module.rank ℂ (LinearMap.range (P (Set.Ioo lam₁ lam₂) : H →ₗ[ℂ] H)) := by sorry

end TeschlQM.MinMax

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 119, Theorem 4.12 (ii)

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)$ .
$P$ assigns a bounded operator $P(\Omega)$ on $\mathcal H$ to each $\Omega\subseteq\mathbb R$ .
$P$ satisfies the imported predicate IsProjValuedMeasure.
$P$ , $\lambda\mapsto\lambda$ and $A$ satisfy the imported predicate IsSpectralIntegral. Neither predicate is unfolded, since their bodies are not part of this text.
$\lambda_1<\lambda_2$ are real numbers.
$k\in\mathbb N$ , and $\psi_1,\dots,\psi_k\in\mathcal D(A)$ are linearly independent over $\mathbb C$ as vectors of $\mathcal H$ .
Let $W=\operatorname{span}_{\mathbb C}\{\psi_1,\dots,\psi_k\}\subseteq\mathcal D(A)$ . For every nonzero $\varphi\in W$ :

\Bigl\|A\varphi - \tfrac{\lambda_1+\lambda_2}{2}\,\varphi\Bigr\| < \tfrac{\lambda_2-\lambda_1}{2}\,\|\varphi\| .

The conclusion is

k\le\dim_{\mathbb C}\operatorname{Ran}P\bigl((\lambda_1,\lambda_2)\bigr),

where the interval is open, $\operatorname{Ran}$ is the range of the operator (no closure taken) and $\dim$ is the cardinal (Hamel) dimension.

Degenerate cases.

$k=0$ . $W=\{0\}$ , the norm hypothesis is vacuous, and the conclusion $0\le\dim$ is trivial.
$\mathcal H=\{0\}$ . Linear independence forces $k=0$ .
Division by 2. The divisions are real divisions by $2$ , so no default values arise.
Consistency of hypotheses. Whether the hypotheses on $P$ and $A$ can hold together depends on the imported predicates.

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