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.

Trace is absolutely convergent and basis independent

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 trace class (Trace class operator). Then:

for every nuclear representation $T x = \sum_{j} ⟨ x, u_{j} ⟩ v_{j}$ of $T$ (operator-norm convergence of the partial sums, $\sum_{j} ∥ u_{j} ∥ ∥ v_{j} ∥ < + \infty$ ), the scalar series $\sum_{j} ⟨ v_{j}, u_{j} ⟩$ converges absolutely and $∣ \sum_{j} ⟨ v_{j}, u_{j} ⟩ ∣ \leq \sum_{j} ∥ u_{j} ∥ ∥ v_{j} ∥;$
the sum $\sum_{j} ⟨ v_{j}, u_{j} ⟩$ depends only on $T$ ; denoting it $tr (T)$ , one has $tr (T) = \sum_{j} ⟨ v_{j}, u_{j} ⟩$ for every nuclear representation of $T$ . This defines $tr (T)$ without assuming that $H$ has a Hilbert basis;
for every supplied Hilbert basis $E$ of $H$ , ${tr}_{E} (T) = tr (T)$ (Trace of a trace class operator);
the trace is linear in the trace-class variable and bounded by the trace norm: for trace-class $S, T$ and scalars $a, b$ , $tr (a S + b T) = a tr (S) + b tr (T)$ and $∣ tr (T) ∣ \leq ∥ T ∥_{1}$ .

Facts & Assumptions

Given: Countable Choice, a Hilbert space $H$ , a trace-class $T \in B (H)$ , its nuclear representations, and the supplied bases.

[A1]

Nuclear representations exist and compute the trace norm. trace class means that $T$ has a nuclear representation; the SVD series is one, and $∥ T ∥_{1} = \sum_{n} s_{n} (T)$ is the infimum of the nuclear sums (Nuclear series characterizes trace norm, Trace class operator, Singular value decomposition for compact operators, Absolute value and singular values of a compact operator).

[A2]

Absolute convergence tools. A nonnegative family has a finite-sum supremum; if the finite subsums are bounded by $C$ then the family is summable with sum at most $C$ , and sums of finite subfamilies of a nonnegative family are bounded by the full sum; for a scalar family, absolute summability implies summability with $∣ \sum ∣ c_{i} ∣$ bound. Suprema over finite subsets of two index sets commute. (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ , Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ )

[A3]

Parseval, Bessel, separable bases. For a Hilbert basis $G$ of a closed subspace $M$ and $w \in M$ , $w = \sum_{g \in G} ⟨ w, g ⟩ g$ with $∥ w ∥^{2} = \sum_{g \in G} ∣ ⟨ w, g ⟩ ∣^{2}$ ; for an orthonormal family and any vector the finite coefficient sums obey Bessel; a closed subspace of $H$ with a given countable dense sequence has a finite or countable Hilbert basis obtained from that sequence by Gram–Schmidt, with no choice (Parseval equivalences for an orthonormal family, Fourier expansion in a Hilbert space, The finite Bessel inequality and best approximation by a finite orthonormal family, A Hilbert space with a dense sequence has a finite or countable orthonormal basis, Orthonormal families, complete orthonormal systems and Hilbert bases, Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets, Finite, countably infinite, countable, uncountable).

[A4]

Cauchy–Schwarz and pairing. $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , the pairing is linear in the first argument and conjugate-linear in the second, and $∥ S v ∥ \leq ∥ S ∥ ∥ v ∥$ (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, Real and complex inner-product spaces and their induced length, A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[A5]

Countable Choice is the standing hypothesis; the deterministic construction below uses no choice beyond it (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

Given: Countable Choice, the trace-class $T$ and nuclear representations $R = ((u_{j}), (v_{j}))$ , $R^{'} = ((u_{j}^{'}), (v_{j}^{'}))$ .

1.1

The candidate scalar is absolutely convergent. For a nuclear representation, $∣ ⟨ v_{j}, u_{j} ⟩ ∣ \leq ∥ u_{j} ∥ ∥ v_{j} ∥$ by [A4], so the scalar series converges absolutely with $∣ \sum_{j} ⟨ v_{j}, u_{j} ⟩ ∣ \leq \sum_{j} ∥ u_{j} ∥ ∥ v_{j} ∥$ by [A2].

A1A2A4

1.2

Comparison of two representations. Put $K_{0} : = \overset{}{span} ({u_{j}} \cup {u_{j}^{'}} \cup {v_{j}} \cup {v_{j}^{'}})$ , listing the finitely many zero families as the constant zero sequence when necessary. Let $F_{0} : = Q$ when $H$ is real and $F_{0} : = Q (i)$ when $H$ is complex. Then $K_{0}$ is a closed subspace with the at most countable dense set of all finite $F_{0}$ -linear combinations of the listed vectors (which exists without choice), so by [A3] it has a finite or countable Hilbert basis $(g_{n})_{n \in N}$ obtained from that sequence by Gram–Schmidt. Both representations show $T (K_{0}) \subseteq K_{0}$ (the value at $x \in K_{0}$ is a norm limit of combinations of the $v_{j}$ , respectively $v_{j}^{'}$ ) and $T x = 0$ for $x ⊥ K_{0}$ (all coefficients $⟨ x, u_{j} ⟩$ , $⟨ x, u_{j}^{'} ⟩$ vanish). For the representation $R$ , expanding both factors in the basis $(g_{n})$ by Parseval [A3] and using absolute convergence and the interchange of nonnegative finite-subset suprema [A2], $\sum_{j} ⟨ v_{j}, u_{j} ⟩ = \sum_{j} \sum_{n} ⟨ v_{j}, g_{n} ⟩ ⟨ g_{n}, u_{j} ⟩ = \sum_{n} \sum_{j} ⟨ v_{j}, g_{n} ⟩ ⟨ g_{n}, u_{j} ⟩ = \sum_{n} ⟨ T g_{n}, g_{n} ⟩$ , the inner identity because $T g_{n} = \sum_{j} ⟨ g_{n}, u_{j} ⟩ v_{j}$ in norm. The same computation applies to $R^{'}$ , so both representations have the same scalar sum; since a trace-class operator has at least one nuclear representation by [A1], the scalar $tr (T) : = \sum_{j} ⟨ v_{j}, u_{j} ⟩$ is well defined and claim 2 holds.

A1A2A3A4

1.3

Agreement with every supplied basis. Let $E$ be a Hilbert basis of $H$ and let $R = ((u_{j}), (v_{j}))$ be any nuclear representation of $T$ . For each $j$ , Parseval in the full space gives $∥ u_{j} ∥^{2} = \sum_{e \in E} ∣ ⟨ u_{j}, e ⟩ ∣^{2}$ and $∥ v_{j} ∥^{2} = \sum_{e \in E} ∣ ⟨ v_{j}, e ⟩ ∣^{2}$ ; hence, by Cauchy–Schwarz for the $e$ -sum, interchange of the nonnegative suprema [A2] and the definition of the representation, $\sum_{e \in E} \sum_{j} ∣ ⟨ e, u_{j} ⟩ ∣ ∣ ⟨ v_{j}, e ⟩ ∣ \leq \sum_{j} ∥ u_{j} ∥ ∥ v_{j} ∥ < + \infty$ . Therefore the double sum $\sum_{e} \sum_{j} ⟨ e, u_{j} ⟩ ⟨ v_{j}, e ⟩$ converges absolutely, its value may be computed in either order, and $\sum_{e \in E} ⟨ T e, e ⟩ = \sum_{e \in E} \sum_{j} ⟨ e, u_{j} ⟩ ⟨ v_{j}, e ⟩ = \sum_{j} \sum_{e \in E} ⟨ e, u_{j} ⟩ ⟨ v_{j}, e ⟩ = \sum_{j} ⟨ v_{j}, u_{j} ⟩$ , the last equality by Parseval applied to the pair $(v_{j}, u_{j})$ in $H$ . This is exactly ${tr}_{E} (T) = tr (T)$ , and it also reproves the absolute summability of $(⟨ T e, e ⟩)$ required by the definition.

A2A3A4

2.1

Linearity and the bound. For trace-class $S, T$ with nuclear representations $R_{S}$ and $R_{T}$ , the concatenation of $R_{S}$ scaled by $a$ and $R_{T}$ scaled by $b$ is a nuclear representation of $a S + b T$ with scalar sum $a \sum ⟨ v_{j}, u_{j} ⟩ + b \sum ⟨ v_{j}^{'}, u_{j}^{'} ⟩$ by absolute convergence, so $tr (a S + b T) = a tr (S) + b tr (T)$ ; and $∣ tr (T) ∣ \leq \sum_{j} ∥ u_{j} ∥ ∥ v_{j} ∥$ for every nuclear representation by [step 1.1], so the infimum characterization [A1] gives $∣ tr (T) ∣ \leq ∥ T ∥_{1}$ .

step 1.1step 1.2A1A2algebra

3.1

Conclusion. Claims 1 and 2 are [step 1.1] and [step 1.2], claim 3 is [step 1.3] and claim 4 is [step 2.1]; the definition of $tr (T)$ uses only nuclear representations of $T$ , so no Hilbert basis of $H$ is assumed to exist, while claim 3 handles every basis that is supplied.

step 1.1step 1.2step 1.3step 2.1A1A5∎

Depends on

Used by

The unilateral shift obstructs a cyclic linear trace extension Counterexample
Fredholm determinant of a trace-class operator Definition
Adjoint, norm and trace of an operator of rank at most one Example
Diagonal Schatten class criteria on ell two Example
Integral operator trace under a valid diagonal hypothesis Example
Fredholm determinant properties for trace-class operators Proposition
Cyclicity of the trace Theorem
Trace of a positive operator is the sum of its eigenvalues Theorem

Dependency tree · two levels

98 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, Lemma 3.27 (printed pp. 97–98) (standard reference, not scraped)
Anthony W. Knapp, Advanced Real Analysis — Chapter II, §5, Proposition 2.8 (standard reference, not scraped)