Alphabeta Math
TheoremStatement: 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.

Spectral theorem for compact self adjoint operators

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let H be a real or complex Hilbert space (Hilbert space) and let TB(H) be a compact self-adjoint operator (Compact linear operator, Self-adjoint, positive, unitary and normal operators, A bounded linear operator between normed spaces). Let

Σ:={λ:λ is an eigenvalue of T, λ0}

be its set of nonzero eigenvalues (Eigenvalues, eigenvectors, eigenspaces Eλ(T)=ker(TλI), and the spectrum σF(T) of an endomorphism), with eigenspaces Eλ=ker(TλI) for λΣ. Then:

  1. Σ is a finite or countably infinite set of real numbers, each eigenvalue has finite multiplicity in the sense dimEλ<+, and for every real ε>0 there are only finitely many λΣ with λε; in particular every point of F{0} has a neighbourhood containing only finitely many elements of Σ, so the only possible accumulation point of Σ is 0;
  2. the closed linear span M of λΣEλ satisfies M=(kerT)=ranT (Orthogonality and the orthogonal complement), and H=MM with MkerT;
  3. for every xH the finite-subset net of λΣλPλx over the orthogonal projections Pλ onto Eλ converges in norm and Tx=λΣλPλx;
  4. if in addition H is a complex Hilbert space, then the nonzero spectrum agrees with the nonzero eigenvalues, σ(T){μC:μ0}=Σ.

No Hilbert basis of kerT is selected anywhere: only the orthonormal bases of the finite-dimensional eigenspaces Eλ, λ0, are used.

Facts & Assumptions

Given: Countable Choice, a real or complex Hilbert space H, a compact self-adjoint TB(H), the set Σ of nonzero eigenvalues, their eigenspaces Eλ=ker(TλI), and M:=spanλΣEλ (the closed linear span).

[A1]

Self-adjointness and eigenspaces. q(x)=Tx,x is real and Tx,y=x,Ty for all x,y; Eλ=ker(TλI) 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 Eλ(T)=ker(TλI), and the spectrum σF(T) of an endomorphism, Linear subspace of a vector space, Kernel and image of a linear map).

[A2]

Extremal eigenvalue and orthogonality. Every nonzero compact self-adjoint operator has S or S 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); Eλ and Eλ are closed T-invariant subspaces on which T satisfies the self-adjoint identity (Orthogonal complement of an eigenspace is invariant).

[A4]

Subspace compactness. If W is a closed subspace of H, the inclusion ι:WH is a bounded linear operator and Tι 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).

[A5]

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).

[A6]

Orthogonal complements and expansion. For every subset S, S is a closed linear subspace; uv means u,v=0 (Orthogonality and the orthogonal complement, Orthogonal complements are closed); M=M for a linear subspace M (The double orthogonal complement of a subspace is its closure); H=MM for closed M, with unique decomposition (Orthogonal decomposition by a closed subspace); the finite-subset net of jx,ejej converges to x for a complete orthonormal family, with Parseval's identity (Fourier expansion in a Hilbert space, Parseval equivalences for an orthonormal family); finite Bessel: jFx,ej2x2 (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 2(I)).

[A7]

Cardinality and Archimedes. Under ACω 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 ACω, Every subset of an at most countable set is at most countable, Finite, countably infinite, countable, uncountable, The Axiom of Countable Choice (ACω)); for every real ε>0 there is a natural n1 with 1/n<ε (For every ε>0 in a complete ordered field there is a natural n1 with 1/n<ε).

[A9]

Spectrum. For a complex Banach space, μρ(T) means μIT is bijective with bounded inverse, σ(T)=Cρ(T), and every eigenvalue lies in σ(T) (Spectrum and resolvent of a bounded operator).

Proof

technique · direct

Given: Countable Choice, the compact self-adjoint T, the set Σ of its nonzero eigenvalues, the eigenspaces Eλ, the closed span M, and the closed unit ball B.

1.1

Nonzero eigenspaces are finite-dimensional. Let λΣ and let C:=T(B), which is compact by [A3]. If xEλ with x1 then Tx=λx, so x=λ1Txλ1T(B)λ1C; thus BEλ:={xEλ:x1}λ1C, and λ1C is compact as a continuous image of a compact set [A3]. The set Eλ is closed [A2], so BEλ is closed in H and hence compact as a closed subset of the compact set λ1C [A3]; by the closed-unit-ball criterion [A5] applied to the normed space Eλ, the space Eλ has finite dimension, so its multiplicity is finite.

A2A3A5
1.2

Only finitely many eigenvalues above each threshold. Fix ε>0 and put Σε:={λΣ:λε}. The compact set C:=T(B) has a finite cover by open balls of radius ε/2 with centres in C, by applying compactness to the cover by all such balls [A3]. For each ball U in that finite cover let LU consist of those λΣε for which TeU for some unit eEλ. If distinct λ,ν belonged to LU, their witnessing unit eigenvectors e,f would be orthogonal by [A2], and hence TeTf2=λ2+ν22ε2, whereas two points of U have distance less than ε. Thus each LU has at most one element. Every λΣε has a unit eigenvector whose image belongs to C, so Σε=ULU is finite. This argument makes no infinite choice of eigenvectors. For a0, the ball B(a,a/2) meets Σ only inside Σa/2, proving local finiteness away from zero.

A1A2A3A8algebra
1.3

M is annihilated by T. Since M is the closed linear span of the subspaces Eλ, a vector is orthogonal to M exactly when it is orthogonal to every Eλ; hence M=λΣEλ is a closed linear subspace, and it is T-invariant because each Eλ is T-invariant [A2]. As a closed subspace of the Hilbert space H, M is complete [A3], and the restriction S:MM is compact: [A4] gives compact closure in H of each bounded image, that closure lies in the closed subspace M, and its subspace topology is unchanged and self-adjoint, since for u,vM one has Tu,v=u,Tv in H and both vectors lie again in M. If S0, the extremal eigenvalue lemma [A2] provides μ=±S0 and wM{0} with Sw=μw, hence Tw=μw and wEμM; then wMM, so w,w=0 and w=0 by positive definiteness, a contradiction. Therefore S=0, that is T vanishes on M.

A1A2A3A4A6
2.1

An orthonormal family with closed span M. By [step 1.2] each set Σ1/(n+1)={λΣ:λ1/(n+1)}, nN, is finite, and every λΣ lies in some Σ1/(n+1) because λ>0 and 1/(n+1)<λ for a suitable n by [A7]; hence Σ=nNΣ1/(n+1) is at most countable by [A7]. By Countable Choice [A7], choose for every λΣ an orthonormal basis (eλ,1,,eλ,dλ) of the finite-dimensional space Eλ, which exists by [A5], and let (ej)jJ be the disjoint union of these finite families indexed by the at most countable set Σ, so that J is at most countable. Every ej has norm 1, and orthonormal bases of orthogonal eigenspaces [A2] make (ej)jJ an orthonormal family whose closed linear span is M by the definition of M.

step 1.2A1A2A5A7
2.2

The support of the operator. Every eigenvector with nonzero eigenvalue is orthogonal to kerT, because for ykerT and xEλ with λ0 one has λx,y=Tx,y=x,Ty=0 by self-adjointness, so x,y=0; since (kerT) is closed [A6] and contains each Eλ, it contains M, while [step 1.3] and [A6] give (kerT)(M)=M=M; hence M=(kerT). Moreover ranT(kerT) by the same computation read with x arbitrary, so ranT(kerT), and if zranT then 0=z,Tx=Tz,x for every x, whence Tz=0 and zkerT; applying [A6] to the linear subspace ranT gives ranT=(ranT)(kerT), while the previous inclusion reverses after taking complements: (kerT)ranT=ranT.

step 1.3A1A6algebra
3.1

The spectral expansion. Let xH. By [A6] and [step 2.2] there is a unique decomposition x=m+n with mM and nM, and by [step 1.3] nkerT, so Tn=0. By [step 2.1] the family (ej) is complete in M, so the Fourier expansion [A6] gives m=jJm,ejej as the limit of the finite-subset net, and the same holds with x,ej in place of m,ej because xmM. Writing Pλx:=i=1dλx,eλ,ieλ,iEλ, the family (Pλx)λΣ is orthogonal with λPλx2x2 by Bessel [A6], so by [A6] the finite-subset net λFPλx converges to some mM; for every j the difference mm is orthogonal to ej, hence to M, so mmMM={0} and m=m. Finally T(λFPλx)=λFλPλx for finite F because each PλxEλ, and continuity of T [A8] carries the convergent net (Pλx) to Tm; hence the finite-subset net of (λPλx) converges to Tm, and adding Tn=0 gives Tx=λΣλPλx.

step 1.3step 2.1step 2.2A1A6A8algebra
3.2

A spectral gap off the eigenvalue set. Let μ0 with μΣ. The set A:={λΣ:λμ/2} is finite by [step 1.2], and μA; set δ:=min({μλ:λA}{μ/2}), a positive real number because A is finite and every displayed distance is positive. For every λΣ one has μλδ: if λμ/2 this is the definition of δ, and if λ<μ/2 then μλμλ>μ/2δ by the triangle inequality [A8]. Consequently, for every zH the orthogonal family ((μλ)1Pλz)λΣ has λμλ2Pλz2δ2λPλz2δ2z2<+ by Bessel [A6], so [A6] makes its finite-subset net converge to a vector of norm δ1z.

step 1.2step 2.1A6A8algebra
4.1

The candidate inverse. Fix μ0 with μΣ and, for zH, write z=m(z)+n(z) with m(z)M, n(z)M as in [step 3.1]. The limit of the finite-subset net in [step 3.2] is unique: if the same net converges to y and to y, then for any ε>0 there are finite sets F0,F1Σ such that every FF0 has aFy<ε/2 and every FF1 has aFy<ε/2; at F=F0F1 the triangle inequality gives yy<ε, and hence y=y. We may therefore define

Az:=λΣ(μλ)1Pλz+μ1n(z),

where the first term is that unique limit. The map A is linear because each Pλ is linear and limits respect linear combinations, and Az2δ2m(z)2+μ2n(z)2max(δ1,μ1)2z2 by orthogonality of the decomposition [A6], so A is a bounded linear operator on H.

step 2.1step 3.2A6A8triangle inequalityalgebra
5.1

The inverse identities and the spectrum. Work now over C and fix μ0 outside Σ. For finite FΣ, put aF(z):=λF(μλ)1Pλz. Since T acts as λI on Eλ, one has (μIT)aF(z)=λFPλz. By [step 3.2] and continuity of μIT, taking limits gives (μIT)limFaF(z)=m(z). Also (μIT)(μ1n(z))=n(z) because Tn(z)=0. Thus (μIT)Az=z. For the other identity, self-adjointness and the finite formula for Pλ give PλTw=λPλw: for each basis vector eEλ, Tw,e=w,Te=λw,e, since λ is real. Moreover TwM by [step 2.2], so n((μIT)w)=μn(w) by uniqueness of the orthogonal decomposition. Consequently A(μIT)w=limFλFPλw+n(w)=m(w)+n(w)=w. This proves that A is a bounded two-sided inverse, so μρ(T) [A9]. Conversely a nonzero eigenvector makes λIT noninjective, so every λΣ lies in σ(T). Therefore σ(T){μ0}=Σ.

step 1.3step 2.2step 3.1step 3.2step 4.1A1A2A6A8A9algebra
6.1

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 kerT selected: the chosen vectors all lie in the eigenspaces Eλ with λ0, which are contained in (kerT) by [step 3.1].

step 1.1step 1.2step 2.1step 2.2step 3.1step 5.1A2

Depends on

Used by

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