TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 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.

Trace of a positive operator is the sum of its eigenvalues

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a real or complex Hilbert space (Hilbert space) and let $T \in B (H)$ be a self-adjoint positive trace-class operator (Self-adjoint, positive, unitary and normal operators, Trace class operator), so that $⟨ T x, x ⟩ \geq 0$ for every $x \in H$ . Let $λ_{1} \geq λ_{2} \geq \dots > 0$ be the positive eigenvalues of $T$ listed with multiplicity (Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism) and let $(s_{n} (T))_{n \geq 1}$ be the zero-padded singular-value sequence (Absolute value and singular values of a compact operator). Then $s_{n} (T) = λ_{n}$ for every $n$ , and $tr (T) = \sum_{n \geq 1} λ_{n} = ∥ T ∥_{1},$ where the sum is over the positive eigenvalues with multiplicity and the equalities are also valid in the finite-rank case (then $λ_{n} : = 0$ for $n$ beyond the rank). This is the positive compact self-adjoint case only; it is not Lidskii's theorem for arbitrary trace-class operators, which is not claimed here.

Facts & Assumptions

Given: Countable Choice, the Hilbert space $H$ , a self-adjoint positive trace-class $T$ , its positive eigenvalues $λ_{n}$ with multiplicity and eigenspaces $E_{λ}$ .

[A1]

Spectral theorem. $T$ is compact self-adjoint; its positive eigenvalues have finite-dimensional eigenspaces, the closed linear span of those eigenspaces is $(\ker T)^{⊥} = \overline{ran T}$ , $H = (\ker T)^{⊥} \oplus \ker T$ , and $T x = \sum_{λ > 0} λ P_{λ} x$ in norm, where $P_{λ}$ is the orthogonal projection onto $E_{λ}$ (Spectral theorem for compact self adjoint operators, Eigenspaces of a self adjoint operator are orthogonal, Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism).

[A2]

Positivity forces nonnegative eigenvalues. If $T v = μ v$ with $v \neq 0$ then $μ ∥ v ∥^{2} = ⟨ T v, v ⟩ \geq 0$ , so $μ \geq 0$ ; and $T$ is self-adjoint with $T^{2} = T^{*} T$ (Self-adjoint, positive, unitary and normal operators, Hilbert-adjoint identities, The Hilbert-space adjoint of a bounded operator, Real and complex inner-product spaces and their induced length).

[A3]

Absolute value of a positive operator. For compact self-adjoint positive $T$ one has $∣ T ∣ = (T^{*} T)^{1 / 2} = (T^{2})^{1 / 2} = T$ , by uniqueness of the compact positive square root applied to the compact self-adjoint positive operator $T$ satisfying $T^{2} = T^{*} T$ (Absolute value and singular values of a compact operator, Positive square root of a compact positive operator).

[A4]

SVD and trace. The singular values of $T$ are the positive eigenvalues of $∣ T ∣$ with multiplicity; the SVD gives orthonormal $(e_{j})_{j \in J}$ in $(\ker T)^{⊥}$ with $∣ T ∣ e_{j} = s_{j} e_{j}$ and $T e_{j} = s_{j} f_{j}$ ; after zero-padding a finite SVD to positive-integer-indexed coefficient families, the trace of a trace-class operator is $\sum_{j \geq 1} ⟨ v_{j}, u_{j} ⟩$ for every nuclear representation $T x = \sum_{j \geq 1} ⟨ x, u_{j} ⟩ v_{j}$ , and $∥ T ∥_{1} = \sum_{n} s_{n} (T)$ (Absolute value and singular values of a compact operator, Singular value decomposition for compact operators, Trace is absolutely convergent and basis independent, Trace class operator, Nuclear series characterizes trace norm).

[A5]

Orthonormal bases of eigenspaces. Every finite-dimensional eigenspace $E_{λ}$ has an orthonormal basis, and orthonormal families consist of unit pairwise orthogonal vectors (Every finite-dimensional real or complex inner product space has an orthonormal basis, Orthonormal families, complete orthonormal systems and Hilbert bases, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

Proof

technique · direct

Given: Countable Choice, the self-adjoint positive trace-class $T$ , its positive eigenvalues with multiplicity and their eigenspaces.

1.1

$∣ T ∣ = T$ . By [A2] $T$ is self-adjoint with $T^{2} = T^{*} T$ , so the compact self-adjoint positive operator $T$ satisfies $T^{2} = T^{*} T$ ; since the positive square root of a compact self-adjoint positive operator is unique by [A3], and $(T^{2})^{1 / 2} = T$ because $T \geq 0$ , the definition $∣ T ∣ = (T^{*} T)^{1 / 2}$ yields $∣ T ∣ = T$ .

A2A3

2.1

The singular values are the positive eigenvalues. By [A1] and [A2] the eigenvalues of $T$ are nonnegative, its positive eigenvalues are exactly the nonzero eigenvalues, and listing them with multiplicity as $λ_{1} \geq λ_{2} \geq \dots > 0$ matches the nonincreasing listing of the positive eigenvalues of $∣ T ∣ = T$ with multiplicity required by [step 1.1]; hence $s_{n} (T) = λ_{n}$ for every $n$ , with zeros appended once the positive eigenvalues are exhausted (the finite-rank case), and $∥ T ∥_{1} = \sum_{n} λ_{n}$ .

step 1.1A1A2A4

3.1

The trace equals the eigenvalue sum. For each positive eigenvalue $λ$ choose an orthonormal basis of $E_{λ}$ by [A5]; the union over the positive eigenvalues is an orthonormal family $(g_{j})_{j \in J}$ whose closed span is $(\ker T)^{⊥}$ by [A1] and [A5]. Since $∣ T ∣ = T$ by [step 1.1], the SVD of $T$ has $e_{j} = g_{j}$ , $s_{j} = λ_{j}$ and $f_{j} = s_{j}^{- 1} T e_{j} = λ_{j}^{- 1} λ_{j} g_{j} = g_{j}$ . For $j \in J$ put $u_{j} = λ_{j} g_{j}$ and $v_{j} = g_{j}$ ; in the finite-rank case $J = {1, \dots, r}$ , extend these to all positive integers by $u_{j} = v_{j} = 0$ for $j > r$ (and use the all-zero families when $r = 0$ ). With $R_{0} = 0$ and $R_{m} = \sum_{j = 1}^{m} ⟨ \cdot, u_{j} ⟩ v_{j}$ , the SVD gives $R_{m} \to T$ in operator norm and $\sum_{j \geq 1} ∥ u_{j} ∥ ∥ v_{j} ∥ = \sum_{j \in J} λ_{j} = ∥ T ∥_{1} < + \infty$ . Thus these positive-integer-indexed families are a nuclear representation in the precise sense of [A4], and its trace formula gives $tr (T) = \sum_{j \geq 1} ⟨ v_{j}, u_{j} ⟩ = \sum_{j \in J} λ_{j} ∥ g_{j} ∥^{2} = \sum_{j \in J} λ_{j}$ .

step 1.1step 2.1A1A4A5

4.1

Conclusion. Steps 2.1 and 3.1 give $s_{n} (T) = λ_{n}$ and $tr (T) = \sum_{n} λ_{n} = ∥ T ∥_{1}$ ; the computation never chooses a basis of $\ker T$ , only orthonormal bases of the finite-dimensional positive eigenspaces, and the identity is stated for self-adjoint positive operators only, as the statement records.

step 2.1step 3.1A1A4∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

88 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.6, positive trace and the eigenvalue sum (printed pp. 97–100) (standard reference, not scraped)
Anthony W. Knapp, Advanced Real Analysis — Chapter II, §5 (standard reference, not scraped)