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.
Absolute value and singular values of a compact operator
Definition
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()). Let and be real or complex Hilbert spaces (Hilbert space) and let be a compact operator (Compact linear operator, A bounded linear operator between normed spaces), with Hilbert adjoint (The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities).
The absolute value. The operator is compact, since it is the composite of the compact with the bounded (Compositions with a compact operator are compact); it is self-adjoint, because (Hilbert-adjoint identities); and it is positive, because for every (Self-adjoint, positive, unitary and normal operators). The absolute value of is the unique compact self-adjoint positive operator with , whose existence and uniqueness are the preceding square-root lemma (Positive square root of a compact positive operator). It satisfies so in particular (The operator norm as the least bound and as the unit-sphere or unit-ball supremum) and , since for every .
The singular values. By the spectral theorem for (Spectral theorem for compact self adjoint operators) the nonzero eigenvalues of form a finite or countably infinite set of positive reals, each with finite multiplicity, and for every real only finitely many of them exceed ; positivity rules out negative eigenvalues and already corresponds to the kernel. The multiset of positive singular values of is the multiset of positive eigenvalues of , counted with multiplicity (Eigenvalues, eigenvectors, eigenspaces , and the spectrum of an endomorphism).
The ordered singular-value sequence. The distinct positive singular values are listed with positive labels in decreasing order as follows: if the multiset of positive eigenvalues is empty (equivalently , equivalently ), the list is empty; otherwise is an eigenvalue of , a maximum and not merely a supremum, because a supremum value not attained would be an accumulation point different from ; having chosen , put is an eigenvalue of and whenever that set is nonempty, and stop otherwise. Each step is legitimate by the finiteness-above-thresholds property above, and an infinite list satisfies (otherwise its decreasing limit would be a nonzero accumulation point). Writing for the multiplicity of (a positive integer), the zero-padded singular-value sequence is where , , and so on; if the multiset is finite with total multiplicity , one sets for every , and if one sets for every . The number is written and called the -th singular value of .
Zero-based domain and positive labels. Set . Thus the numerical sequence is the function on all of , including zero. The positive-labelled tail is the multiplicity-counting list constructed above. The auxiliary initial value is not an additional entry of the eigenvalue multiset, does not index a singular vector, and is excluded from multiplicity counts and singular-value sums, which use . The full sequence satisfies and tends to zero. This preserves the page's positive rank labels while giving convergence statements a zero-based domain.
Rank and the finiteness of the list. The map given by is well defined and linear, because forces and hence ; it is injective, because gives and ; it is surjective onto because ; and it is isometric, . Hence is finite-dimensional if and only if is finite-dimensional; in that case the linear bijection gives (Finite-dimensional vector space, and its dimension ; infinite-dimensional means having no finite basis). Consequently, whenever has finite rank, the positive singular values with multiplicity number exactly , the rank of , and all later vanish, so the sequence is zero-padded. If does not have finite rank, the multiset of positive singular values is infinite and countable (Finite, countably infinite, countable, uncountable) and for every , with ; in particular finite rank of is characterised by the eventual vanishing for all sufficiently large , and conversely such eventual vanishing forces finite rank. The sequence is numerical data only: no orthonormal system is selected here, and the zero padding is not an indexing of any family of vectors. The unordered multiset determines uniquely, so is well defined, and .
Depends on
Spectral theorem for compact self adjoint operators
Positive square root of a compact positive operator
Hilbert-adjoint identities
The Hilbert-space adjoint of a bounded operator
Self-adjoint, positive, unitary and normal operators
Compositions with a compact operator are compact
Compact linear operator
Eigenvalues, eigenvectors, eigenspaces , and the spectrum of an endomorphism
Finite-dimensional vector space, and its dimension ; infinite-dimensional means having no finite basis
Orthogonality and the orthogonal complement
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
Real and complex inner-product spaces and their induced length
Finite, countably infinite, countable, uncountable
The Axiom of Countable Choice ()