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 class iff product of two Hilbert Schmidt operators

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ and $K$ be real or complex Hilbert spaces (Hilbert space), let $E$ be a Hilbert basis of $H$ and $G$ a Hilbert basis of $K$ (both supplied as data), and let $T \in B (H, K)$ be compact (Compact linear operator). Then:

(factorization of a trace-class operator) if $T$ is trace class (Trace class operator), then, with $∣ T ∣$ , $U$ and the singular system of $T$ (Absolute value and singular values of a compact operator, Singular value decomposition for compact operators), the operators $B : = ∣ T ∣^{1 / 2} \in B (H), A : = U ∣ T ∣^{1 / 2} \in B (H, K)$ satisfy $T = A B$ , are both Hilbert–Schmidt relative to $E$ (Hilbert–Schmidt operator and Hilbert–Schmidt norm), and $∥ A ∥_{H S, E} = ∥ B ∥_{H S, E} = ∥ T ∥_{1}^{1 / 2},$ so that $∥ A ∥_{H S, E} ∥ B ∥_{H S, E} = ∥ T ∥_{1}$ : the trace norm is attained by this factorization;
(products of Hilbert–Schmidt operators are trace class) conversely, if there are a real or complex Hilbert space $H_{0}$ with a supplied Hilbert basis $E_{0}$ , a Hilbert–Schmidt operator $B \in B (H, H_{0})$ relative to $E$ and a Hilbert–Schmidt operator $A \in B (H_{0}, K)$ relative to $E_{0}$ with $T = A B$ , then $T$ is trace class and $∥ T ∥_{1} \leq ∥ A ∥_{H S, E_{0}} ∥ B ∥_{H S, E};$ in particular $A B$ is compact and $∥ T ∥ \leq ∥ A ∥_{H S, E_{0}} ∥ B ∥_{H S, E}$ .

The bases $E$ , $E_{0}$ , $G$ are supplied data; no existence of a Hilbert basis is asserted or used, and the adjoint-stability of the Hilbert–Schmidt norm across $G$ is the imported invariance theorem.

Facts & Assumptions

Given: Countable Choice, Hilbert spaces $H, H_{0}, K$ , supplied Hilbert bases $E$ of $H$ , $E_{0}$ of $H_{0}$ , $G$ of $K$ , and a compact $T \in B (H, K)$ .

[A1]

Trace norm. $T$ is trace class exactly when $\sum_{n} s_{n} (T) < + \infty$ , and then $∥ T ∥_{1} = \sum_{n} s_{n} (T)$ and $∥ T ∥ = s_{1} (T) \leq ∥ T ∥_{1}$ (Trace class operator, Absolute value and singular values of a compact operator).

[A2]

SVD and the positive square root. With $J$ the index set of positive singular values, $T x = \sum_{j \in J} s_{j} ⟨ x, e_{j} ⟩ f_{j}$ in norm, $∣ T ∣ e_{j} = s_{j} e_{j}$ , $(e_{j})$ and $(f_{j})$ orthonormal, $U$ is the partial isometry with $U e_{j} = f_{j}$ on $(\ker T)^{⊥}$ extended by zero on $\ker T$ , $U ∣ T ∣ = T$ , and $U$ is isometric on $(\ker T)^{⊥}$ with range $\overline{ran T}$ ; moreover $∣ T ∣ = \sum_{j} s_{j} ⟨ \cdot, e_{j} ⟩ e_{j}$ . Since $∣ T ∣$ is compact, self-adjoint and positive, it has a compact self-adjoint positive square root $∣ T ∣^{1 / 2}$ , which acts by $s_{j}^{1 / 2}$ on each $e_{j}$ and by zero on $\ker T$ (Singular value decomposition for compact operators, Absolute value and singular values of a compact operator, Positive square root of a compact positive operator).

[A3]

Hilbert–Schmidt calculus. The Hilbert–Schmidt norm is basis-independent and adjoint-stable, and $∥ S B ∥_{H S} \leq ∥ S ∥ ∥ B ∥_{H S}$ for bounded $S$ ; a Hilbert–Schmidt operator is compact; composites of compact operators with bounded ones are compact (Hilbert Schmidt operators form a two sided ideal, The Hilbert–Schmidt norm is basis independent, Hilbert–Schmidt operators are compact, Hilbert–Schmidt operator and Hilbert–Schmidt norm, Compositions with a compact operator are compact, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[A4]

Parseval, Bessel, collapse of suprema. For a Hilbert basis and any vector, the squared norm is the sum of the squared moduli of the coefficients; Bessel's inequality bounds finite coefficient sums for orthonormal families; for nonnegative families indexed by two sets the finite-subset suprema may be interchanged, $\sup_{F, G} \sum_{e \in F, j \in G} c_{e, j} = \sup_{G, F} \sum_{j \in G, e \in F} c_{e, j}$ (Parseval equivalences for an orthonormal family, The finite Bessel inequality and best approximation by a finite orthonormal family, Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ , Orthonormal families, complete orthonormal systems and Hilbert bases).

[A5]

Cauchy–Schwarz and boundedness. $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ and the pairing is linear in the first argument and conjugate-linear in the second; $∥ S v ∥ \leq ∥ S ∥ ∥ v ∥$ and $∥ S T ∥ \leq ∥ S ∥ ∥ T ∥$ (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, Hilbert-adjoint identities, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

Proof

technique · direct

1.1

Products of Hilbert–Schmidt operators are trace class. Assume $T = A B$ with $B \in B (H, H_{0})$ Hilbert–Schmidt relative to $E$ and $A \in B (H_{0}, K)$ Hilbert–Schmidt relative to $E_{0}$ . Then $B$ is compact [A3], so $T = A B$ is compact [A3] and [A2] applies to $T$ with singular system $(e_{j}, f_{j}, s_{j})_{j \in J}$ ; for every finite $F \subseteq J$ , and writing $⟨ T e_{j}, f_{j} ⟩ = ⟨ A B e_{j}, f_{j} ⟩ = ⟨ B e_{j}, A^{*} f_{j} ⟩$ [A5], finite Cauchy–Schwarz in $C^{F}$ gives $\sum_{j \in F} s_{j} = \sum_{j \in F} ⟨ T e_{j}, f_{j} ⟩ \leq (\sum_{j \in F} ∥ B e_{j} ∥^{2})^{1 / 2} (\sum_{j \in F} ∥ A^{*} f_{j} ∥^{2})^{1 / 2} \leq ∥ B ∥_{H S, E} ∥ A^{*} ∥_{H S, G} = ∥ B ∥_{H S, E} ∥ A ∥_{H S, E_{0}}$ , the last inequality because $(e_{j})$ is an orthonormal family in $H$ with a Hilbert basis $E$ available so $\sum_{j \in F} ∥ B e_{j} ∥^{2} \leq \sum_{e \in E} ∥ B e ∥^{2}$ by Bessel and Parseval [A4], and likewise for $(f_{j})$ and $A^{*}$ ; the equality is the adjoint-stability of the Hilbert–Schmidt norm [A3]. Taking the supremum over finite $F$ gives $∥ T ∥_{1} = \sum_{j} s_{j} \leq ∥ B ∥_{H S, E} ∥ A ∥_{H S, E_{0}} < + \infty$ , so $T$ is trace class with the asserted bound, and $∥ T ∥ \leq ∥ T ∥_{1}$ is [A1].

A1A2A3A4A5

1.2

The Hilbert–Schmidt norms of the two factors of a trace-class operator. Assume now that $T$ is trace class and put $B : = ∣ T ∣^{1 / 2}$ , $A : = U ∣ T ∣^{1 / 2}$ . First, $B$ is self-adjoint with $B^{2} = ∣ T ∣$ and $B$ kills $\ker T$ and preserves $(\ker T)^{⊥} = [span {e_{j} : j \in J}]^{closure}$ [A2], so $B e_{j} = s_{j}^{1 / 2} e_{j}$ and $∣ T ∣ e = \sum_{j} s_{j} ⟨ e, e_{j} ⟩ e_{j}$ for every $e \in H$ . Hence for the fixed Hilbert basis $E$ of $H$ , using Parseval for each $e_{j}$ and the interchange of nonnegative suprema [A4], $\sum_{e \in E} ∥ B e ∥^{2} = \sum_{e \in E} ⟨ ∣ T ∣ e, e ⟩ = \sum_{e \in E} \sum_{j} s_{j} ∣ ⟨ e, e_{j} ⟩ ∣^{2} = \sum_{j} s_{j} \sum_{e \in E} ∣ ⟨ e, e_{j} ⟩ ∣^{2} = \sum_{j} s_{j} ∥ e_{j} ∥^{2} = \sum_{j} s_{j} = ∥ T ∥_{1} < + \infty$ , so $B$ is Hilbert–Schmidt relative to $E$ with $∥ B ∥_{H S, E}^{2} = ∥ T ∥_{1}$ [A1]. Second, by [A2] every $B e = ∣ T ∣^{1 / 2} e$ lies in $(\ker T)^{⊥}$ , on which $U$ is isometric with values in $\overline{ran T}$ , so $∥ A e ∥ = ∥ U B e ∥ = ∥ B e ∥$ for every $e \in E$ ; therefore $\sum_{e \in E} ∥ A e ∥^{2} = \sum_{e \in E} ∥ B e ∥^{2} = ∥ T ∥_{1}$ , so $A$ is Hilbert–Schmidt relative to $E$ with $∥ A ∥_{H S, E}^{2} = ∥ T ∥_{1}$ as well. Finally $A B = U ∣ T ∣^{1 / 2} ∣ T ∣^{1 / 2} = U ∣ T ∣ = T$ by [A2].

A1A2A4algebra

2.1

Conclusion. Claim 2 is [step 1.1], claim 1 is [step 1.2]; the factorization of [step 1.2] has $H_{0} = H$ and $E_{0} = E$ and attains equality $∥ A ∥_{H S} ∥ B ∥_{H S} = ∥ T ∥_{1}$ because both norms equal $∥ T ∥_{1}^{1 / 2}$ .

step 1.1step 1.2∎

Depends on

Used by

Cyclicity of the trace Theorem

Dependency tree · two levels

117 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.26 (printed pp. 95–97) (standard reference, not scraped)
Anthony W. Knapp, Advanced Real Analysis — Chapter II, §5, Propositions 2.8–2.9 (standard reference, not scraped)