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.
Trace of a trace class operator
Definition
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()). Let be a real or complex Hilbert space (Hilbert space), let be a trace-class operator on (Trace class operator) and let be a Hilbert basis of , supplied as data (Orthonormal families, complete orthonormal systems and Hilbert bases; existence of such a basis is not asserted here). The trace of relative to is the sum of the scalar family in the finite-subset-net sense of Square-summable families on an arbitrary index set and the space .
The family is absolutely summable, uniformly in . Let be the singular-value series (Singular value decomposition for compact operators, Absolute value and singular values of a compact operator) with , orthonormal and (Trace class operator). For every the series converges absolutely, because the moduli are bounded by by Cauchy–Schwarz and Bessel (Cauchy–Schwarz: , with equality exactly for dependent pairs, The finite Bessel inequality and best approximation by a finite orthonormal family). Consequently, for every finite , using the interchange of finite sums with the nonnegative finite-subset supremum over and then finite Cauchy–Schwarz and Bessel twice, because for each the two finite coefficient sums are bounded by and (finite Bessel). Hence the finite subsums of are bounded by , the family is absolutely summable, and an absolutely summable family of scalars is summable in ZF with (Square-summable families on an arbitrary index set and the space ). This justifies the notation before any basis-independence statement.
Choice accounting and status. Only a supplied basis and the singular values of are used; no Hilbert basis of is assumed to exist, and the next theorem proves that does not depend on the supplied basis and equals the basis-free trace of (Trace is absolutely convergent and basis independent).
Depends on
Trace class operator
Absolute value and singular values of a compact operator
Singular value decomposition for compact operators
Nuclear series characterizes trace norm
Square-summable families on an arbitrary index set and the space
The finite Bessel inequality and best approximation by a finite orthonormal family
Cauchy–Schwarz: , with equality exactly for dependent pairs
Orthonormal families, complete orthonormal systems and Hilbert bases
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
Convergence of a sequence in a metric space: iff in
The Axiom of Countable Choice ()