LemmaStatement: 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.

Nuclear series characterizes trace norm

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ and $K$ be Hilbert spaces over the same real or complex scalar field and let $T \in B (H, K)$ be compact (Compact linear operator). Then $T$ is trace class (Trace class operator) if and only if there are families $(u_{j})_{j \geq 1}$ in $H$ and $(v_{j})_{j \geq 1}$ in $K$ , indexed by the positive integers, with $\sum_{j \geq 1} ∥ u_{j} ∥ ∥ v_{j} ∥ < + \infty$ such that the zero-based sequence of finite-rank operators defined by $R_{0} = 0$ and $R_{m} : = \sum_{j = 1}^{m} ⟨ \cdot, u_{j} ⟩ v_{j} (m \geq 1)$ converges to $T$ in operator norm (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ). Here the displayed scalar series is, under the library convention, the series of the sequence $(∥ u_{m + 1} ∥ ∥ v_{m + 1} ∥)_{m \in N}$ . In that case $∥ T ∥_{1} = \inf {\sum_{j \geq 1} ∥ u_{j} ∥ ∥ v_{j} ∥ : R_{m} \to T in operator norm},$ the infimum being over all such nuclear representations of $T$ , with the same zero-based shift understood in every displayed sum, and the infimum is attained: using its positive-integer index set and padding finite rank by zeros, the singular-value series $T = \sum_{j \in J} s_{j} ⟨ \cdot, e_{j} ⟩ f_{j}$ is a nuclear representation with sum $∥ T ∥_{1}$ .

Facts & Assumptions

Given: Countable Choice, real or complex Hilbert spaces $H, K$ over the same field, and compact $T \in B (H, K)$ . Nuclear data are assumed only in the reverse implication.

[A1]

The SVD has $J = {1, 2, \dots}$ in infinite rank and $J = {1, \dots, r}$ in rank $r$ , including $J = \emptyset$ when $r = 0$ . It supplies orthonormal $(e_{j}), (f_{j})$ , $T e_{j} = s_{j} f_{j}$ , and operator-norm convergence of $T_{m} = \sum_{j \in J, j \leq m} s_{j} ⟨ \cdot, e_{j} ⟩ f_{j}$ to $T$ (Singular value decomposition for compact operators, Absolute value and singular values of a compact operator).

[A2]

Trace class and its norm are defined by the sum of the zero-padded positive-indexed singular values, equivalently by the zero-indexed sequence $(s_{m + 1} (T))_{m \in N}$ (Trace class operator).

[A3]

The operator norm bounds $∥ S x ∥ \leq ∥ S ∥ ∥ x ∥$ , and norm convergence means these norms of differences tend to zero (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: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

[A5]

The pairing is linear in the first argument and conjugate-linear in the second. Cauchy–Schwarz gives $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , and finite Bessel sums are bounded by the squared norm (Real and complex inner-product spaces and their induced length, Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, The finite Bessel inequality and best approximation by a finite orthonormal family).

[A6]

An infimum is a greatest lower bound; a member of a set that is also a lower bound is consequently its infimum (Greatest lower bound (infimum)).

[A7]

A nondecreasing real sequence bounded above converges to the supremum of its range (A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum).

Proof

technique · direct

1.1

Suppose $T$ is trace class. For every $j \in J$ set $u_{j} = s_{j} e_{j}$ and $v_{j} = f_{j}$ . Because $s_{j}$ is real, conjugate-linearity gives $⟨ x, s_{j} e_{j} ⟩ = s_{j} ⟨ x, e_{j} ⟩$ . In finite rank put $u_{j} = v_{j} = 0$ for $j > r$ ; in rank zero use zero families throughout. In infinite rank $J$ already consists of all positive integers, so no index shift and no vector $e_{0}$ is used. Orthonormality gives $∥ u_{j} ∥ ∥ v_{j} ∥ = s_{j}$ for $j \in J$ . The shifted zero-based sum is $∥ T ∥_{1} < \infty$ , and the zero-based partial-sum sequence with $R_{0} = 0$ converges in operator norm by [A1].

A1A2A5assume-hyp

1.2

Conversely assume given positive-integer-indexed families with $C = \sum_{j \geq 1} ∥ u_{j} ∥ ∥ v_{j} ∥ < \infty$ in the shifted sense just specified, and let the zero-based sequence $(R_{m})_{m \in N}$ converge to $T$ in operator norm. Each term is linear and bounded by $∥ u_{j} ∥ ∥ v_{j} ∥$ using [A5], so $R_{m}$ is bounded and its range lies in the finite span of $v_{1}, \dots, v_{m}$ (the zero subspace when $m = 0$ ). The given compactness of $T$ licenses [A1]; no new compactness theorem is needed.

givenA1A3A5assume-hyp

2.1

Fix a finite $F \subseteq J$ . Since $T e_{k} = s_{k} f_{k}$ , put $S_{F} = \sum_{k \in F} s_{k} = \sum_{k \in F} ⟨ T e_{k}, f_{k} ⟩$ . For every $m \in N$ , finite rearrangement (with the sum empty at $m = 0$ ) gives $a_{m} : = \sum_{k \in F} ⟨ R_{m} e_{k}, f_{k} ⟩ = \sum_{j = 1}^{m} \sum_{k \in F} ⟨ e_{k}, u_{j} ⟩ ⟨ v_{j}, f_{k} ⟩ .$ Finite Cauchy–Schwarz, applied to the vectors of absolute values in $R^{∣ F ∣}$ , and Bessel give $∣ \sum_{k \in F} ⟨ e_{k}, u_{j} ⟩ ⟨ v_{j}, f_{k} ⟩ ∣ \leq {(\sum_{k \in F} ∣ ⟨ u_{j}, e_{k} ⟩ ∣^{2})}^{1 / 2} {(\sum_{k \in F} ∣ ⟨ v_{j}, f_{k} ⟩ ∣^{2})}^{1 / 2} \leq ∥ u_{j} ∥ ∥ v_{j} ∥ .$ Thus $∣ a_{m} ∣ \leq C$ . Also $∣ S_{F} - a_{m} ∣ \leq ∣ F ∣ ∥ T - R_{m} ∥$ by [A3] and [A5], so the zero-based sequence $(a_{m})$ converges to $S_{F}$ and $S_{F} \leq C$ . For empty $F$ this says $0 \leq C$ ; otherwise a hypothetical $S_{F} > C$ contradicts the displayed error bound for sufficiently large $m$ .

step 1.2A1A3A5algebra

3.1

Take $F = J \cap {1, \dots, n}$ for each $n \in N$ . The zero-padded singular-value partial sums are nondecreasing, start at zero, and are bounded above by $C$ by step 2.1. Therefore [A7] makes their series converge to a value at most $C$ . By [A2], $T$ is trace class and $∥ T ∥_{1} \leq C$ .

step 2.1A2A7

4.1

Steps 1.1 and 3.1 prove the equivalence. For trace-class $T$ , the set of nuclear-representation sums is nonempty by step 1.1, every such sum is at least $∥ T ∥_{1}$ by step 3.1, and step 1.1 attains this bound. It is therefore the infimum by [A6]. All sequences used in the reverse implication were given; the forward implication spends only the Countable Choice already assumed by the SVD.

step 1.1step 3.1A6∎

Depends on

Used by

Fredholm determinant of a trace-class operator Definition
Trace of a trace class operator Definition
Adjoint, norm and trace of an operator of rank at most one Example
Integral operator trace under a valid diagonal hypothesis Example
Cyclicity of the trace Theorem
Trace class is a two sided Banach operator ideal Theorem
Trace is absolutely convergent and basis independent Theorem
Trace of a positive operator is the sum of its eigenvalues Theorem

Dependency tree · two levels

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