Theorem 4.12 (i) — ⟨ψ, Aψ⟩ < λ‖ψ‖² on a k-dimensional span forces dim Ran P_A((−∞, λ)) ≥ k

Proved

TeschlQM.MinMax.dim_range_ge_of_form

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$ and form domain $\mathfrak Q(A)$ , and let $\psi_1, \dots, \psi_k \in \mathfrak Q(A)$ be linearly independent. Let $\lambda \in \mathbb R$ . If

\langle \psi, A\psi \rangle < \lambda \|\psi\|^2

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

\dim \operatorname{Ran} P_A((-\infty, \lambda)) \ge k .

Similarly, if $\langle \psi, A\psi \rangle > \lambda\|\psi\|^2$ for every such $\psi$ , then $\dim \operatorname{Ran} P_A((\lambda, \infty)) \ge k$ .

A $k$ -dimensional space of trial functions on which the expectation of $A$ stays below $\lambda$ thus certifies at least $k$ dimensions of spectral subspace below $\lambda$ .

Formalization Note. The spectral theorem is not formalized here: the projection-valued measure $P$ is taken as data with the hypothesis that $A = \int \lambda\, dP(\lambda)$ (IsSpectralIntegral P (fun x => x) A), so $P_A = P$ . For $\psi \in \mathfrak Q(A)$ , $\langle\psi, A\psi\rangle$ is the quadratic form $q_A(\psi) = \int \eta \, d\mu_\psi(\eta)$ (quadForm P ψ). Dimensions are cardinals (Module.rank), so an infinite-dimensional range satisfies the bound. The Hilbert space is not assumed separable.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_IsProjValuedMeasure
import Definitions.Def_TeschlQM_Shared_IsSpectralIntegral
import Definitions.Def_TeschlQM_MinMax_formDomain

Formal statement

namespace TeschlQM.MinMax

/-- Teschl, Theorem 4.12 (i), p. 119, (4.33)–(4.34): let `A` be self-adjoint with
projection-valued measure `P` (i.e. `A = ∫ λ dP(λ)`, so `P_A = P`), let `ψ₁, …, ψ_k` be linearly
independent elements of the form domain `𝔔(A)` and `λ ∈ ℝ`. If `⟨ψ, Aψ⟩ < λ‖ψ‖²` (the quadratic
form `q_A(ψ) = ∫ η dμ_ψ(η)`) for every nonzero linear combination `ψ` of the `ψ_j`, then
`dim Ran P_A((−∞, λ)) ≥ k`; similarly `⟨ψ, Aψ⟩ > λ‖ψ‖²` implies `dim Ran P_A((λ, ∞)) ≥ k`.
Dimensions are cardinals (`Module.rank`). -/
theorem dim_range_ge_of_form {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)
    {k : ℕ} (ψ : Fin k → H) (hli : LinearIndependent ℂ ψ) (hQ : ∀ j, ψ j ∈ formDomain P)
    (lam : ℝ) :
    ((∀ φ ∈ Submodule.span ℂ (Set.range ψ), φ ≠ 0 → quadForm P φ < lam * ‖φ‖ ^ 2) →
        (k : Cardinal) ≤ Module.rank ℂ (LinearMap.range (P (Set.Iio lam) : H →ₗ[ℂ] H))) ∧
      ((∀ φ ∈ Submodule.span ℂ (Set.range ψ), φ ≠ 0 → lam * ‖φ‖ ^ 2 < quadForm P φ) →
        (k : Cardinal) ≤ Module.rank ℂ (LinearMap.range (P (Set.Ioi lam) : H →ₗ[ℂ] H))) := by sorry

end TeschlQM.MinMax

Source

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

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 set $\Omega\subseteq\mathbb R$ .
$P$ satisfies the imported predicate IsProjValuedMeasure.
$P$ , the function $\lambda\mapsto\lambda$ (as a complex number) and $A$ together satisfy the imported predicate IsSpectralIntegral.
$k\in\mathbb N$ , and $\psi_1,\dots,\psi_k\in\mathcal H$ are linearly independent over $\mathbb C$ .
Each $\psi_j$ belongs to $\mathfrak Q(P)$ , the imported formDomain P.
$\lambda\in\mathbb R$ is arbitrary.

$q(\varphi)$ denotes the imported real-valued quadForm P φ. None of the imported definitions is unfolded here, because their bodies are not part of this declaration's text. Let $W=\operatorname{span}_{\mathbb C}\{\psi_1,\dots,\psi_k\}$ . The conclusion is the conjunction of two implications:

If $q(\varphi)<\lambda\|\varphi\|^2$ for every nonzero $\varphi\in W$ , then

k\le\dim_{\mathbb C}\operatorname{Ran}P\bigl((-\infty,\lambda)\bigr).

If $\lambda\|\varphi\|^2<q(\varphi)$ for every nonzero $\varphi\in W$ , then

k\le\dim_{\mathbb C}\operatorname{Ran}P\bigl((\lambda,\infty)\bigr).

Dimensions are cardinal (Hamel) dimensions of the ranges of the operators, with no closure taken. Both conditions use $q$ built from $P$ ; $A$ does not appear in them. The conditions are imposed on all of $W$ , which may contain vectors not in $\mathfrak Q(P)$ , since only the $\psi_j$ themselves are assumed to lie there.

Degenerate cases.

$k=0$ . $W=\{0\}$ , both premises hold vacuously, and both conclusions reduce to $0\le\dim$ , which is trivially true.
$\mathcal H=\{0\}$ . Linear independence forces $k=0$ .
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