Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-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 of a trace class operator

Definition

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let H be a real or complex Hilbert space (Hilbert space), let T∈B(H) be a trace-class operator on H (Trace class operator) and let E be a Hilbert basis of H, supplied as data (Orthonormal families, complete orthonormal systems and Hilbert bases; existence of such a basis is not asserted here). The trace of T relative to E is tr⁡E(T):=∑e∈E⟨Te,e⟩, the sum of the scalar family (⟨Te,e⟩)e∈E in the finite-subset-net sense of Square-summable families on an arbitrary index set and the space ℓ2(I).

The family is absolutely summable, uniformly in E. Let T=∑jsj⟨⋅,ej⟩fj be the singular-value series (Singular value decomposition for compact operators, Absolute value and singular values of a compact operator) with (ej)j∈J, (fj)j∈J orthonormal and ∑jsj=∥T∥1<+∞ (Trace class operator). For every e∈H the series ⟨Te,e⟩=∑jsj⟨e,ej⟩⟨fj,e⟩ converges absolutely, because the moduli are bounded by s1∑j∣⟨e,ej⟩⟨fj,e⟩∣≤s1∥e∥2 by Cauchy–Schwarz and Bessel (Cauchy–Schwarz: ∣⟨x,y⟩∣≤∥x∥ ∥y∥, with equality exactly for dependent pairs, The finite Bessel inequality and best approximation by a finite orthonormal family). Consequently, for every finite F⊆E, using the interchange of finite sums with the nonnegative finite-subset supremum over j and then finite Cauchy–Schwarz and Bessel twice, ∑e∈F∣⟨Te,e⟩∣≤∑e∈F∑jsj∣⟨e,ej⟩∣ ∣⟨fj,e⟩∣=∑jsj∑e∈F∣⟨e,ej⟩∣ ∣⟨fj,e⟩∣≤∑jsj(∑e∈F∣⟨e,ej⟩∣2)1/2(∑e∈F∣⟨fj,e⟩∣2)1/2≤∑jsj=∥T∥1, because for each j the two finite coefficient sums are bounded by ∥ej∥=1 and ∥fj∥=1 (finite Bessel). Hence the finite subsums of ∣(⟨Te,e⟩)∣e∈E are bounded by ∥T∥1, the family is absolutely summable, and an absolutely summable family of scalars is summable in ZF with ∣∑e∈E⟨Te,e⟩∣≤∥T∥1 (Square-summable families on an arbitrary index set and the space ℓ2(I)). This justifies the notation tr⁡E(T) before any basis-independence statement.

Choice accounting and status. Only a supplied basis E and the singular values of T are used; no Hilbert basis of H is assumed to exist, and the next theorem proves that tr⁡E(T) does not depend on the supplied basis and equals the basis-free trace of T (Trace is absolutely convergent and basis independent).

Depends on

Dependency tree · 2 levels

Sources