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.
Lidskii trace formula for trace-class operators
Statement
proof uses external results not yet established in this library
Assume the Axiom of Choice. Let be any complex Hilbert space, including , and let . List all nonzero eigenvalues with their finite algebraic multiplicities, where the multiplicity of is the dimension of the stabilized generalized kernel . Then The list is finite or countable and may be empty. No normality, self-adjointness, positivity, or separability of is assumed.
Facts & Assumptions
Given: The Axiom of Choice, a complex Hilbert space , and a trace-class operator .
The determinant definition preserves the nonzero generalized-eigenvalue data under separable-support reduction (Fredholm determinant of a trace-class operator).
The determinant properties give absolute eigenvalue summability, locally uniformly, and (Fredholm determinant properties for trace-class operators).
Proof
By [F1] and [F2], the eigenvalue list has the stated algebraic multiplicities and . For a finite initial product , expansion and the ordered-tuple bound for elementary symmetric sums give . Indeed, every unordered product of distinct absolute eigenvalues occurs times among the ordered -tuples contributing to .
Let . The local product convergence and absolute convergence of from [F2] preserve the bound in step 1.1, so . The left side is by [F2]. The same argument applies to finite and empty lists, with the empty sum equal to and the empty product equal to .
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
24 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
- Aleksey Kostenko, Trace Ideals with Applications — Theorem 3.4.7, printed p. 41 (standard reference, not scraped)