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.
Spectral theorem for compact self adjoint operators
Statement
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()). Let be a real or complex Hilbert space (Hilbert space) and let be a compact self-adjoint operator (Compact linear operator, Self-adjoint, positive, unitary and normal operators, A bounded linear operator between normed spaces). Let
be its set of nonzero eigenvalues (Eigenvalues, eigenvectors, eigenspaces , and the spectrum of an endomorphism), with eigenspaces for . Then:
- is a finite or countably infinite set of real numbers, each eigenvalue has finite multiplicity in the sense , and for every real there are only finitely many with ; in particular every point of has a neighbourhood containing only finitely many elements of , so the only possible accumulation point of is ;
- the closed linear span of satisfies (Orthogonality and the orthogonal complement), and with ;
- for every the finite-subset net of over the orthogonal projections onto converges in norm and
- if in addition is a complex Hilbert space, then the nonzero spectrum agrees with the nonzero eigenvalues,
No Hilbert basis of is selected anywhere: only the orthonormal bases of the finite-dimensional eigenspaces , , are used.
Facts & Assumptions
Given: Countable Choice, a real or complex Hilbert space , a compact self-adjoint , the set of nonzero eigenvalues, their eigenspaces , and (the closed linear span).
Self-adjointness and eigenspaces. is real and for all ; is the eigenspace of and is a linear subspace (Self-adjoint, positive, unitary and normal operators, The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities, Eigenvalues, eigenvectors, eigenspaces , and the spectrum of an endomorphism, Linear subspace of a vector space, Kernel and image of a linear map).
Extremal eigenvalue and orthogonality. Every nonzero compact self-adjoint operator has or as an eigenvalue with a unit eigenvector (Norm point of a compact self adjoint operator is an eigenvalue up to sign); eigenvalues of a self-adjoint operator are real and distinct eigenspaces are orthogonal (Eigenspaces of a self adjoint operator are orthogonal); and are closed -invariant subspaces on which satisfies the self-adjoint identity (Orthogonal complement of an eigenspace is invariant).
Compactness and closed subspaces. is compact exactly when is a compact subset of , where (Compact linear operator, Open ball, closed ball and sphere in a metric space); scalar multiples and continuous images of compact sets are compact (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism); a closed subset of a compact space is compact (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact); a compact metric space is sequentially compact, choice-free (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); a closed subspace of a complete metric space is complete, in ZF (Closed subspaces of complete metric spaces are complete; the converse under countable choice); is a Banach space (Banach space, A bounded linear operator between normed spaces).
Subspace compactness. If is a closed subspace of , the inclusion is a bounded linear operator and is compact (Compositions with a compact operator are compact, A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).
Finite dimension. A normed space has compact closed unit ball exactly when it admits an ordered basis of finite length (The closed unit ball is compact if and only if the normed space is finite-dimensional); every finite-dimensional real or complex inner product space has an orthonormal basis, the empty one in dimension zero (Every finite-dimensional real or complex inner product space has an orthonormal basis); an orthonormal family is linearly independent with unit vectors (Orthonormal families, complete orthonormal systems and Hilbert bases).
Orthogonal complements and expansion. For every subset , is a closed linear subspace; means (Orthogonality and the orthogonal complement, Orthogonal complements are closed); for a linear subspace (The double orthogonal complement of a subspace is its closure); for closed , with unique decomposition (Orthogonal decomposition by a closed subspace); the finite-subset net of converges to for a complete orthonormal family, with Parseval's identity (Fourier expansion in a Hilbert space, Parseval equivalences for an orthonormal family); finite Bessel: (The finite Bessel inequality and best approximation by a finite orthonormal family); a square-summable orthogonal family has a norm-convergent finite-subset net whose limit has the sums of the squared norms (Square-summable orthogonal families have norm-convergent finite sums, Square-summable families on an arbitrary index set and the space ).
Cardinality and Archimedes. Under a countable union of at most countable sets is at most countable, and subsets of at most countable sets are at most countable (Countable unions of at most countable sets, assuming , Every subset of an at most countable set is at most countable, Finite, countably infinite, countable, uncountable, The Axiom of Countable Choice ()); for every real there is a natural with (For every in a complete ordered field there is a natural with ).
Continuity, limits, scalars. Bounded linear operators are continuous with (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 are unique (Convergence of a sequence in a metric space: iff in , A sequence in a metric space has at most one limit); the complex distance is (The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane); the inner product is additive and homogeneous in the first argument (Real and complex inner-product spaces and their induced length).
Spectrum. For a complex Banach space, means is bijective with bounded inverse, , and every eigenvalue lies in (Spectrum and resolvent of a bounded operator).
Proof
Given: Countable Choice, the compact self-adjoint , the set of its nonzero eigenvalues, the eigenspaces , the closed span , and the closed unit ball .
Nonzero eigenspaces are finite-dimensional. Let and let , which is compact by [A3]. If with then , so ; thus , and is compact as a continuous image of a compact set [A3]. The set is closed [A2], so is closed in and hence compact as a closed subset of the compact set [A3]; by the closed-unit-ball criterion [A5] applied to the normed space , the space has finite dimension, so its multiplicity is finite.
Only finitely many eigenvalues above each threshold. Fix and put . The compact set has a finite cover by open balls of radius with centres in , by applying compactness to the cover by all such balls [A3]. For each ball in that finite cover let consist of those for which for some unit . If distinct belonged to , their witnessing unit eigenvectors would be orthogonal by [A2], and hence , whereas two points of have distance less than . Thus each has at most one element. Every has a unit eigenvector whose image belongs to , so is finite. This argument makes no infinite choice of eigenvectors. For , the ball meets only inside , proving local finiteness away from zero.
is annihilated by . Since is the closed linear span of the subspaces , a vector is orthogonal to exactly when it is orthogonal to every ; hence is a closed linear subspace, and it is -invariant because each is -invariant [A2]. As a closed subspace of the Hilbert space , is complete [A3], and the restriction is compact: [A4] gives compact closure in of each bounded image, that closure lies in the closed subspace , and its subspace topology is unchanged and self-adjoint, since for one has in and both vectors lie again in . If , the extremal eigenvalue lemma [A2] provides and with , hence and ; then , so and by positive definiteness, a contradiction. Therefore , that is vanishes on .
An orthonormal family with closed span . By [step 1.2] each set , , is finite, and every lies in some because and for a suitable by [A7]; hence is at most countable by [A7]. By Countable Choice [A7], choose for every an orthonormal basis of the finite-dimensional space , which exists by [A5], and let be the disjoint union of these finite families indexed by the at most countable set , so that is at most countable. Every has norm , and orthonormal bases of orthogonal eigenspaces [A2] make an orthonormal family whose closed linear span is by the definition of .
The support of the operator. Every eigenvector with nonzero eigenvalue is orthogonal to , because for and with one has by self-adjointness, so ; since is closed [A6] and contains each , it contains , while [step 1.3] and [A6] give ; hence . Moreover by the same computation read with arbitrary, so , and if then for every , whence and ; applying [A6] to the linear subspace gives , while the previous inclusion reverses after taking complements: .
The spectral expansion. Let . By [A6] and [step 2.2] there is a unique decomposition with and , and by [step 1.3] , so . By [step 2.1] the family is complete in , so the Fourier expansion [A6] gives as the limit of the finite-subset net, and the same holds with in place of because . Writing , the family is orthogonal with by Bessel [A6], so by [A6] the finite-subset net converges to some ; for every the difference is orthogonal to , hence to , so and . Finally for finite because each , and continuity of [A8] carries the convergent net to ; hence the finite-subset net of converges to , and adding gives .
A spectral gap off the eigenvalue set. Let with . The set is finite by [step 1.2], and ; set , a positive real number because is finite and every displayed distance is positive. For every one has : if this is the definition of , and if then by the triangle inequality [A8]. Consequently, for every the orthogonal family has by Bessel [A6], so [A6] makes its finite-subset net converge to a vector of norm .
The candidate inverse. Fix with and, for , write with , as in [step 3.1]. The limit of the finite-subset net in [step 3.2] is unique: if the same net converges to and to , then for any there are finite sets such that every has and every has ; at the triangle inequality gives , and hence . We may therefore define
where the first term is that unique limit. The map is linear because each is linear and limits respect linear combinations, and by orthogonality of the decomposition [A6], so is a bounded linear operator on .
The inverse identities and the spectrum. Work now over and fix outside . For finite , put . Since acts as on , one has . By [step 3.2] and continuity of , taking limits gives . Also because . Thus . For the other identity, self-adjointness and the finite formula for give : for each basis vector , , since is real. Moreover by [step 2.2], so by uniqueness of the orthogonal decomposition. Consequently . This proves that is a bounded two-sided inverse, so [A9]. Conversely a nonzero eigenvector makes noninjective, so every lies in . Therefore .
Conclusion. Claim 1 is the combination of [step 1.1], [step 1.2], [step 2.1] and the reality of eigenvalues in [A2]; claim 2 is [step 2.2] together with the decomposition of [step 3.1]; claim 3 is [step 3.1]; claim 4 is [step 5.1]. At no point was a Hilbert basis of selected: the chosen vectors all lie in the eigenspaces with , which are contained in by [step 3.1].
Depends on
- Norm point of a compact self adjoint operator is an eigenvalue up to sign
- Eigenspaces of a self adjoint operator are orthogonal
- Orthogonal complement of an eigenspace is invariant
- Self-adjoint, positive, unitary and normal operators
- Hilbert-adjoint identities
- The Hilbert-space adjoint of a bounded operator
- Compact linear operator
- Spectrum and resolvent of a bounded operator
- Eigenvalues, eigenvectors, eigenspaces $E_\lambda(T)=\ker(T-\lambda I)$, and the spectrum $\sigma_F(T)$ of an endomorphism
- 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
- The closed unit ball is compact if and only if the normed space is finite-dimensional
- A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact
- A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism
- Compositions with a compact operator are compact
- Orthogonal decomposition by a closed subspace
- The double orthogonal complement of a subspace is its closure
- Fourier expansion in a Hilbert space
- Parseval equivalences for an orthonormal family
- The finite Bessel inequality and best approximation by a finite orthonormal family
- Square-summable orthogonal families have norm-convergent finite sums
- Square-summable families on an arbitrary index set and the space $\ell^2(I)$
- Orthonormal families, complete orthonormal systems and Hilbert bases
- Every finite-dimensional real or complex inner product space has an orthonormal basis
- Orthogonality and the orthogonal complement
- Orthogonal complements are closed
- Real and complex inner-product spaces and their induced length
- Hilbert space
- The operator norm as the least bound and as the unit-sphere or unit-ball supremum
- A bounded linear operator between normed spaces
- For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent
- Convergence of a sequence in a metric space: $x_k \to x$ iff $d(x_k, x) \to 0$ in $\mathbb{R}$
- A sequence in a metric space has at most one limit
- Open ball, closed ball and sphere in a metric space
- Closed subspaces of complete metric spaces are complete; the converse under countable choice
- Countable unions of at most countable sets, assuming $\mathrm{AC}_\omega$
- Every subset of an at most countable set is at most countable
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- Finite, countably infinite, countable, uncountable
- Linear subspace of a vector space
- Kernel and image of a linear map
- The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane
- Banach space
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
- Orthonormal eigenbasis for a compact self adjoint operator Corollary
- Absolute value and singular values of a compact operator Definition
- Adjoint, norm and trace of an operator of rank at most one Example
- Positive square root of a compact positive operator Lemma
- Spectral convolution eigenspaces are finite-dimensional and invariant Lemma
- Singular value decomposition for compact operators Theorem
- Trace of a positive operator is the sum of its eigenvalues Theorem
Dependency tree · two levels
166 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.7 and Corollaries 3.8–3.9 (printed pp. 74–78) (standard reference, not scraped)
- Anthony W. Knapp, Advanced Real Analysis — Chapter II, §2, Theorem 2.3 (standard reference, not scraped)