Lemma 6.22 — a relatively compact operator has A-bound zero

Proved

TeschlQM.Weyl.relativeBound_eq_zero

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

compact-operatorsfunctional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1perturbation-theory

Let $A$ be a self-adjoint operator in a complex Hilbert space $\mathfrak H$ and suppose $K$ is relatively compact with respect to $A$ . Then the $A$ -bound of $K$ is zero:

\inf\{ a \ge 0 \mid \exists b \ge 0\ \forall \psi \in \mathfrak D(A):\ \|K\psi\| \le a\|A\psi\| + b\|\psi\| \} = 0 .

Relatively compact perturbations are therefore infinitesimally small, and the Kato–Rellich theorem applies to them with any bound.

Formalization Note. The $A$ -bound is valued in $[0,\infty]$ and equals $\infty$ when $K$ is not $A$ bounded, so the conclusion includes that $K$ is $A$ bounded. Relative compactness is (5.12): $K R_A(z)$ is compact for one $z \in \rho(A)$ , with $\mathfrak D(A) \subseteq \mathfrak D(K)$ .

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_resolventSet
import Definitions.Def_TeschlQM_Shared_IsRelativelyCompact
import Definitions.Def_TeschlQM_Shared_relativeBound

Formal statement

namespace TeschlQM.Weyl

/-- Teschl, Lemma 6.22, p. 148. Let `A` be self-adjoint and suppose `K` is relatively compact with
respect to `A`. Then the `A`-bound of `K` is zero. (The `A`-bound is valued in `[0, ∞]` and is `∞`
for an operator that is not `A` bounded, so the conclusion includes that `K` is `A` bounded.) -/
theorem relativeBound_eq_zero {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] (A K : H →ₗ.[ℂ] H) (hA : IsSelfAdjoint A) (hK : TeschlQM.Shared.IsRelativelyCompact K A) :
    TeschlQM.Shared.relativeBound A K = 0 := by sorry

end TeschlQM.Weyl

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 148, Lemma 6.22

Read-back

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

Setting. $H$ is a complex Hilbert space. $A$ and $K$ are partially defined $\mathbb{C}$ -linear operators on $H$ .

Hypotheses.

$A^* = A$ , with the library's adjoint of a partially defined operator. That adjoint is the usual one for dense $\mathcal{D}(A)$ . Otherwise it is the zero operator on all of $H$ , so the hypothesis then forces $A = 0$ on all of $H$ .
$K$ is relatively compact with respect to $A$ , in the sense of the imported predicate TeschlQM.Shared.IsRelativelyCompact K A. Its definition is not shown here.

No symmetry or domain condition is imposed on $K$ other than what that predicate contains.

Conclusion. The $A$ -bound of $K$ equals $0$ :

\mathrm{relativeBound}(A, K) = 0,

where $\mathrm{relativeBound}(A, K)$ is the imported definition TeschlQM.Shared.relativeBound A K. Its definition, and the set it takes values in, are not shown here.

Degenerate cases. Whether the conclusion is informative when $K$ is not $A$ -bounded, or when a defining set is empty or unbounded, depends entirely on how the imported relativeBound treats those cases, and that is not visible in this text. If $H = \{0\}$ , the statement asserts the value $0$ for whatever the imported definition returns there.

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