CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 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.

Orthonormal eigenbasis for a compact self adjoint operator

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $H$ be a real or complex Hilbert space (Hilbert space) and let $T \in B (H)$ be a compact self-adjoint operator (Compact linear operator, Self-adjoint, positive, unitary and normal operators). Then $T$ has a Hilbert basis (Orthonormal families, complete orthonormal systems and Hilbert bases) consisting of eigenvectors of $T$ (Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism): one may take the union of orthonormal bases of the finitely many-dimensional nonzero eigenspaces with a Hilbert basis of $\ker T$ . If $\ker T = {0}$ no vectors from the kernel are needed, and if all nonzero eigenspaces are absent (that is $T = 0$ ) the union is a Hilbert basis of $H = \ker T$ .

Facts & Assumptions

Given: AC, a real or complex Hilbert space $H$ , a compact self-adjoint $T$ , the set $Σ$ of its nonzero eigenvalues, the eigenspaces $E_{λ}$ for $λ \in Σ$ , and $M : = \overset{}{span} ⋃_{λ \in Σ} E_{λ}$ .

[A1]

Spectral theorem. $Σ$ is finite or countably infinite with finite multiplicities, the nonzero eigenvalues are real and distinct eigenspaces are orthogonal, $M = (\ker T)^{⊥} = \overline{ran T}$ and $H = M \oplus M^{⊥}$ with $M^{⊥} = \ker T$ (Spectral theorem for compact self adjoint operators, Eigenspaces of a self adjoint operator are orthogonal, Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism).

[A2]

Orthonormal families. An orthonormal family has unit vectors which are pairwise orthogonal, and every finite-dimensional real or complex inner product space has an orthonormal basis, the empty one in dimension zero; the closed linear span of an orthonormal family is a closed subspace, and a Hilbert basis is a complete orthonormal family (Orthonormal families, complete orthonormal systems and Hilbert bases, Every finite-dimensional real or complex inner product space has an orthonormal basis).

[A3]

Complements. $S^{⊥}$ is a closed linear subspace for every subset $S$ ; orthogonality is symmetric and bilinear in the obvious sense; for closed $M$ one has $H = M \oplus M^{⊥}$ with $M^{⊥ ⊥} = M$ (Orthogonality and the orthogonal complement, Orthogonal complements are closed, Orthogonal decomposition by a closed subspace).

[A4]

Zorn and AC data. Under AC every nonempty poset in which every chain has an upper bound has a maximal element (Zorn's lemma, The Axiom of Choice, Partial order and partially ordered set, Chain in a poset, Upper bound, least upper bound, and strict upper bound, Maximal element and greatest element); AC implies ${A C}_{ω}$ (AC supplies the countable and dependent choices used in Banach integration, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[A5]

Closed subspaces are complete. A closed subspace of a complete metric space is complete in ZF, so a closed subspace of a Hilbert space is again a Hilbert space (Closed subspaces of complete metric spaces are complete; the converse under countable choice, Hilbert space). The set of orthonormal families in a subset of $H$ is a poset under inclusion, and the inclusion-union of a chain of orthonormal families is orthonormal (Orthonormal families, complete orthonormal systems and Hilbert bases, Partial order and partially ordered set, Chain in a poset).

Proof

technique · direct

Given: AC, the compact self-adjoint $T$ , the nonzero eigenspaces $E_{λ}$ , their closed span $M$ , and the kernel $K_{0} : = \ker T$ .

1.1

An orthonormal family spanning $M$ . For every $λ \in Σ$ the eigenspace $E_{λ}$ is finite-dimensional by [A1], so it has an orthonormal basis by [A2]; the disjoint union $E$ of all these finite bases is an orthonormal family, because each basis is orthonormal and vectors belonging to distinct eigenvalues are orthogonal by [A1]. Its closed linear span is $M$ by the definition of $M$ , and $M = (\ker T)^{⊥}$ by [A1].

A1A2

1.2

A maximal orthonormal family in the kernel. Let $P$ be the set of orthonormal families contained in $\ker T$ , ordered by inclusion. This is a nonempty poset (the empty family belongs to it) and the union of any chain in $P$ is again an orthonormal family contained in $\ker T$ , hence an upper bound of the chain; therefore Zorn's lemma [A4] provides a maximal element $B \in P$ .

A2A4A5

2.1

$B$ is complete in the kernel. Let $W : = \overset{}{span} B \subseteq \ker T$ be the closed span of $B$ , which is a closed subspace of the Hilbert space $\ker T$ [A5]; if $W \neq \ker T$ then by the orthogonal decomposition in the Hilbert space $\ker T$ [A3] there is $v \in \ker T \cap W^{⊥}$ with $v \neq 0$ . Then $v / ∥ v ∥$ has norm $1$ , is orthogonal to every element of $B$ , and lies in $\ker T$ , so $B \cup {v / ∥ v ∥}$ is an orthonormal family in $\ker T$ strictly containing $B$ , contradicting maximality; hence $W = \ker T$ , that is $B$ is a complete orthonormal family of the Hilbert space $\ker T$ .

step 1.2A2A3A5

3.1

The union is a Hilbert basis of $H$ . The union $E \cup B$ is an orthonormal family: it is the union of two orthonormal families, and every $b \in B \subseteq \ker T$ is orthogonal to every $e \in E \subseteq M = (\ker T)^{⊥}$ by [step 1.1] and [A1]. Its closed linear span contains $M$ (by [step 1.1]) and $\ker T$ (by [step 2.1]), hence contains $M \oplus \ker T = H$ by [A1]; therefore $E \cup B$ is complete and is a Hilbert basis of $H$ .

step 1.1step 2.1A1A2A3

4.1

Conclusion. Every element of $E \cup B$ is an eigenvector of $T$ : the vectors of $E$ lie in nonzero eigenspaces, while every $b \in B$ is a unit vector in $\ker T$ , so $b \neq 0$ and $T b = 0 = 0 b$ (Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism). Thus, whenever $B$ is nonempty, $0$ is an eigenvalue witnessed by each of its members; when $\ker T = {0}$ one has $B = \emptyset$ , and the proof neither needs nor asserts that $0$ is an eigenvalue. By [step 3.1] the family $E \cup B$ is a Hilbert basis of $H$ consisting of eigenvectors of $T$ , which proves the corollary; the degenerate descriptions in the statement are the cases $M = {0}$ (then $E = \emptyset$ and $B$ spans $\ker T = H$ ) and $\ker T = {0}$ (then $B = \emptyset$ ).

step 3.1A1A2A4∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

90 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, Corollary 3.9 (printed p. 78) (standard reference, not scraped)
Anthony W. Knapp, Advanced Real Analysis — Chapter II, §2, Theorem 2.3 (standard reference, not scraped)