Alphabeta Math
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 (ACω)). 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∈B(H,K) be compact (Compact linear operator). Then:

  1. (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∈B(H),A:=U∣T∣1/2∈B(H,K) satisfy T=AB, are both Hilbert–Schmidt relative to E (Hilbert–Schmidt operator and Hilbert–Schmidt norm), and ∥A∥HS,E=∥B∥HS,E=∥T∥11/2, so that ∥A∥HS,E∥B∥HS,E=∥T∥1: the trace norm is attained by this factorization;
  2. (products of Hilbert–Schmidt operators are trace class) conversely, if there are a real or complex Hilbert space H0 with a supplied Hilbert basis E0, a Hilbert–Schmidt operator B∈B(H,H0) relative to E and a Hilbert–Schmidt operator A∈B(H0,K) relative to E0 with T=AB, then T is trace class and ∥T∥1≤∥A∥HS,E0∥B∥HS,E; in particular AB is compact and ∥T∥≤∥A∥HS,E0∥B∥HS,E.

The bases E, E0, 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,H0,K, supplied Hilbert bases E of H, E0 of H0, G of K, and a compact T∈B(H,K).

[A1]

Trace norm. T is trace class exactly when ∑nsn(T)<+∞, and then ∥T∥1=∑nsn(T) and ∥T∥=s1(T)≤∥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, Tx=∑j∈Jsj⟨x,ej⟩fj in norm, ∣T∣ej=sjej, (ej) and (fj) orthonormal, U is the partial isometry with Uej=fj on (ker⁡T)⊥ extended by zero on ker⁡T, U∣T∣=T, and U is isometric on (ker⁡T)⊥ with range ran⁡T‾; moreover ∣T∣=∑jsj⟨⋅,ej⟩ej. Since ∣T∣ is compact, self-adjoint and positive, it has a compact self-adjoint positive square root ∣T∣1/2, which acts by sj1/2 on each ej 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 ∥SB∥HS≤∥S∥∥B∥HS 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∑e∈F,j∈Gce,j=sup⁡G,F∑j∈G,e∈Fce,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⟩∣≤∥u∥∥v∥ and the pairing is linear in the first argument and conjugate-linear in the second; ∥Sv∥≤∥S∥∥v∥ and ∥ST∥≤∥S∥∥T∥ (Cauchy–Schwarz: ∣⟨x,y⟩∣≤∥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: xk→x iff d(xk,x)→0 in R).

Proof

technique · direct
1.1A1A2A3A4A5

Products of Hilbert–Schmidt operators are trace class. Assume T=AB with B∈B(H,H0) Hilbert–Schmidt relative to E and A∈B(H0,K) Hilbert–Schmidt relative to E0. Then B is compact [A3], so T=AB is compact [A3] and [A2] applies to T with singular system (ej,fj,sj)j∈J; for every finite F⊆J, and writing ⟨Tej,fj⟩=⟨ABej,fj⟩=⟨Bej,A∗fj⟩ [A5], finite Cauchy–Schwarz in CF gives ∑j∈Fsj=∑j∈F⟨Tej,fj⟩≤(∑j∈F∥Bej∥2)1/2(∑j∈F∥A∗fj∥2)1/2≤∥B∥HS,E∥A∗∥HS,G=∥B∥HS,E∥A∥HS,E0, the last inequality because (ej) is an orthonormal family in H with a Hilbert basis E available so ∑j∈F∥Bej∥2≤∑e∈E∥Be∥2 by Bessel and Parseval [A4], and likewise for (fj) and A∗; the equality is the adjoint-stability of the Hilbert–Schmidt norm [A3]. Taking the supremum over finite F gives ∥T∥1=∑jsj≤∥B∥HS,E∥A∥HS,E0<+∞, so T is trace class with the asserted bound, and ∥T∥≤∥T∥1 is [A1].

1.2A1A2A4algebra

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 B2=∣T∣ and B kills ker⁡T and preserves (ker⁡T)⊥=[span⁡{ej:j∈J}]closure [A2], so Bej=sj1/2ej and ∣T∣e=∑jsj⟨e,ej⟩ej for every e∈H. Hence for the fixed Hilbert basis E of H, using Parseval for each ej and the interchange of nonnegative suprema [A4], ∑e∈E∥Be∥2=∑e∈E⟨∣T∣e,e⟩=∑e∈E∑jsj∣⟨e,ej⟩∣2=∑jsj∑e∈E∣⟨e,ej⟩∣2=∑jsj∥ej∥2=∑jsj=∥T∥1<+∞, so B is Hilbert–Schmidt relative to E with ∥B∥HS,E2=∥T∥1 [A1]. Second, by [A2] every Be=∣T∣1/2e lies in (ker⁡T)⊥, on which U is isometric with values in ran⁡T‾, so ∥Ae∥=∥UBe∥=∥Be∥ for every e∈E; therefore ∑e∈E∥Ae∥2=∑e∈E∥Be∥2=∥T∥1, so A is Hilbert–Schmidt relative to E with ∥A∥HS,E2=∥T∥1 as well. Finally AB=U∣T∣1/2∣T∣1/2=U∣T∣=T by [A2].

2.1step 1.1step 1.2∎

Conclusion. Claim 2 is [step 1.1], claim 1 is [step 1.2]; the factorization of [step 1.2] has H0=H and E0=E and attains equality ∥A∥HS∥B∥HS=∥T∥1 because both norms equal ∥T∥11/2.

Depends on

Used by

Dependency tree · two levels

118 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