LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Norm point of a compact self adjoint operator is an eigenvalue up to sign

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a real or complex Hilbert space (Hilbert space) and let $T \in B (H)$ be a nonzero compact self-adjoint operator (Compact linear operator, Self-adjoint, positive, unitary and normal operators, A bounded linear operator between normed spaces). Then either $∥ T ∥$ or $- ∥ T ∥$ is an eigenvalue of $T$ (Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism) and possesses a unit eigenvector; here $∥ T ∥ > 0$ .

Facts & Assumptions

Given: Countable Choice, a nonzero compact self-adjoint operator $T$ on a Hilbert space $H$ , and the quadratic form $q (x) = ⟨ T x, x ⟩$ .

[A1]

Norm formula and positivity of the norm. $∥ T ∥ = \sup {∣ q (x) ∣ : ∥ x ∥ = 1}$ with the empty-supremum convention; $T \neq 0$ forces $H \neq {0}$ and $∥ T ∥ > 0$ , and for every real $ε > 0$ there is a unit vector $u$ with $∣ q (u) ∣ > ∥ T ∥ - ε$ (Norm of a self adjoint operator from its quadratic form, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[A2]

Self-adjointness. $q$ is real-valued and $⟨ T x, y ⟩ = ⟨ x, T y ⟩$ for all $x, y$ , so $∥ T v ∥^{2} = ⟨ T v, T v ⟩ = ⟨ T^{2} v, v ⟩$ for every $v \in H$ (Self-adjoint, positive, unitary and normal operators, The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities).

[A3]

Compactness and ZF metrisation. compactness of $T$ is tested on the closed unit ball: for compact $T$ the set $\overline{T (\overline{B})}$ is a compact subset of $H$ , and conversely a compact closure of that image forces $T$ to be compact, where $\overline{B} = {x \in H : ∥ x ∥ \leq 1}$ is the closed unit ball; a compact metric space is sequentially compact, and that implication is a theorem of ZF (Compact linear operator, In any metric space compactness implies countable compactness and limit point compactness, and each of countable compactness and limit point compactness implies sequential compactness; every implication here is proved without a choice principle).

[A4]

Continuity, norms and limits. Bounded linear operators are continuous and satisfy $∥ T v ∥ \leq ∥ T ∥ ∥ v ∥$ (A bounded linear operator between normed spaces, For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent, The operator norm as the least bound and as the unit-sphere or unit-ball supremum); limits of sequences in a metric space are unique, convergence of norms gives $∥ x_{n} ∥ \to ∥ x ∥$ , and a continuous map carries convergent sequences to convergent sequences (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , A sequence in a metric space has at most one limit).

[A5]

Choice and enumeration. Countable Choice supplies one unit vector for each $n \in N$ from the nonempty set ${u : ∥ u ∥ = 1, ∣ q (u) ∣ > ∥ T ∥ - 1 / (n + 1)}$ ; the increasing enumeration of an infinite subset of $N$ is defined by recursion and is choice-free (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The recursion theorem, The well-ordering principle).

[A6]

Eigenvalues. A scalar $λ$ is an eigenvalue of $T$ when $T x = λ x$ for some $x \neq 0$ , and such an $x$ is a unit eigenvector when in addition $∥ x ∥ = 1$ (Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism).

Proof

technique · direct

Given: Countable Choice, a nonzero compact self-adjoint $T$ , its quadratic form $q$ , and the closed unit ball $\overline{B}$ .

1.1

Approximate maximisers. For each $n \in N$ , the number $∥ T ∥ - 1 / (n + 1)$ is strictly below the supremum in [A1], so the set $X_{n} : = {u \in H : ∥ u ∥ = 1, ∣ q (u) ∣ > ∥ T ∥ - 1 / (n + 1)}$ is nonempty. Countable Choice [A5] supplies a function $x : N \to H$ with $x_{n} \in X_{n}$ for every $n \in N$ . Thus $(x_{n})_{n \in N}$ is a zero-based sequence of unit vectors with the required bound.

A1A5

2.1

A constant sign on a subsequence. Put $P : = N$ and $A : = {n \in P : q (x_{n}) \geq 0}$ . Since the infinite set $P$ is the union of $A$ and $P ∖ A$ , at least one of those two sets is infinite. If $A$ is infinite let $n_{0} < n_{1} < \dots$ be its increasing enumeration and set $λ : = ∥ T ∥$ ; otherwise let $n_{0} < n_{1} < \dots$ enumerate the infinite set $P ∖ A$ and set $λ : = - ∥ T ∥$ . In either case every $n_{k} \in N$ , so $x_{n_{k}}$ is defined. Then $λ \in {- ∥ T ∥, ∥ T ∥}$ and for every $k$ , because $q (x_{n_{k}})$ has the sign of $λ$ on this subsequence and $∣ λ ∣ = ∥ T ∥$ , $λ q (x_{n_{k}}) = ∥ T ∥ ∣ q (x_{n_{k}}) ∣ \geq ∥ T ∥ (∥ T ∥ - 1 / (n_{k} + 1))$ and $λ^{2} = ∥ T ∥^{2}$ .

step 1.1A1A5algebra

2.2

A convergent image subsequence. The set $C : = \overline{T (\overline{B})}$ is compact by compactness of $T$ [A3], and $T x_{n_{k}} \in C$ for every $k$ because $∥ x_{n_{k}} ∥ = 1$ by [step 1.1], so by sequential compactness of the compact metric space $C$ [A3] there are a strictly increasing sequence $k_{0} < k_{1} < \dots$ and a point $y \in C$ with $T x_{n_{k_{j}}} \to y$ .

step 1.1A3

3.1

The residual tends to zero. For every $k$ , using [A2], $∥ x_{n_{k}} ∥ = 1$ and [step 2.1], $∥ (T - λ I) x_{n_{k}} ∥^{2} = ∥ T x_{n_{k}} ∥^{2} - 2 λ q (x_{n_{k}}) + λ^{2} \leq ∥ T ∥^{2} - 2 ∥ T ∥ (∥ T ∥ - 1 / (n_{k} + 1)) + ∥ T ∥^{2} = 2 ∥ T ∥ / (n_{k} + 1)$ , the inequality using $∥ T x_{n_{k}} ∥ \leq ∥ T ∥$ ; since $n_{k} \geq k$ and $∥ T ∥$ is fixed, $∥ (T - λ I) x_{n_{k}} ∥ \to 0$ .

step 2.1step 2.2A1A2A4algebra

4.1

The approximating vectors converge. For each $j$ the identity $x_{n_{k_{j}}} = λ^{- 1} (T x_{n_{k_{j}}} - (T - λ I) x_{n_{k_{j}}})$ holds because $λ \neq 0$ (indeed $∣ λ ∣ = ∥ T ∥ > 0$ by [A1]); the first term converges to $λ^{- 1} y$ by [step 2.2] and the second to $0$ by [step 3.1], so $x_{n_{k_{j}}} \to x : = λ^{- 1} y$ .

step 2.2step 3.1algebra

5.1

Conclusion. By continuity of the norm and $∥ x_{n_{k_{j}}} ∥ = 1$ we get $∥ x ∥ = 1$ [A4], and by continuity of $T$ and uniqueness of limits $T x_{n_{k_{j}}} \to T x$ while also $T x_{n_{k_{j}}} \to y = λ x$ , so $T x = λ x$ ; thus $λ \in {- ∥ T ∥, ∥ T ∥}$ is an eigenvalue of $T$ with the unit eigenvector $x$ .

step 4.1A4A6∎

Depends on

Used by

Dependency tree · two levels

86 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §3.2, Theorem 3.6 (printed pp. 73–74) (standard reference, not scraped)
Anthony W. Knapp, Advanced Real Analysis — Chapter II, §2, Theorem 2.3 (standard reference, not scraped)