Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 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.

The Hilbert–Schmidt norm is basis independent

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) and let T∈B(H,K) be a bounded linear operator (A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum), with Hilbert adjoint T∗∈B(K,H) (The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities). Let E be a Hilbert basis of H and F a Hilbert basis of K (Orthonormal families, complete orthonormal systems and Hilbert bases), and let sE(T)=∑e∈E∥Te∥2 and sF(T∗)=∑f∈F∥T∗f∥2 be the finite-subset-supremum sums of Hilbert–Schmidt operator and Hilbert–Schmidt norm and Square-summable families on an arbitrary index set and the space ℓ2(I). Then:

  1. (matrix-coefficient form) the finite-subset supremum sup⁡{∑e∈A∑f∈B∣⟨Te,f⟩∣2  :  A⊆E, B⊆F finite} equals sE(T), and it also equals sF(T∗);
  2. (basis independence) sE(T)=sE′(T) for every Hilbert basis E′ of H, and sE(T)=sF(T∗) for every Hilbert basis F of K;
  3. (membership and norms) T is Hilbert–Schmidt relative to E if and only if it is Hilbert–Schmidt relative to every other Hilbert basis of H, and then ∥T∥HS,E=∥T∥HS,E′=∥T∗∥HS,F for all such bases E,E′ and every Hilbert basis F of K; when the common defining sum is +∞, none of these Hilbert–Schmidt norms is defined, and T is Hilbert–Schmidt relative to none of the bases.

Facts & Assumptions

Given: Countable Choice, bounded T:H→K, a Hilbert basis E of H and a Hilbert basis F of K.

[F1]

Since F is a complete orthonormal family in the Hilbert space K, every y∈K satisfies ∥y∥2=∑f∈F∣⟨y,f⟩∣2, the sum being the finite-subset supremum; similarly for E in H (Parseval equivalences for an orthonormal family, Orthonormal families, complete orthonormal systems and Hilbert bases).

[F2]

The Hilbert adjoint satisfies ⟨Tx,y⟩=⟨x,T∗y⟩ for all x∈H, y∈K, it is the unique such bounded operator, and T∗f∈H for every f∈K (The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities).

[F3]

For a fixed finite set A, fix one bijection q:n→A with a von Neumann natural n (The cardinality ∣A∣ of a finite set). Given nonempty sets Ce for e∈A, apply Every natural-number-indexed list of nonempty sets has a choice function on its family of values to the function k↦Cq(k) on n. Its choice function c on the set of values yields be=c(Ce)∈Ce. This transports finite choice to this fixed A; no enumeration of the entire basis or simultaneous choice of enumerations is asserted.

[F4]

For a nonnegative family (ce)e∈E the sum is the supremum of the finite subsums, is monotone in the family, and satisfies ∑e∈Ece=∑e∈Fce+∑e∈E∖Fce for finite F⊆E (Square-summable families on an arbitrary index set and the space ℓ2(I)).

[F5]

Countable Choice is the hypothesis under which Parseval and the adjoint interface are available (The Axiom of Countable Choice (ACω)).

[F6]

The operator T is Hilbert–Schmidt relative to E exactly when sE(T)<+∞, and then ∥T∥HS,E=(sE(T))1/2; the same definitions apply to E′ and to T∗ with respect to F (Hilbert–Schmidt operator and Hilbert–Schmidt norm).

Proof

technique · direct

Given: Countable Choice, bounded T:H→K, Hilbert bases E of H and F of K, and the nonnegative numbers ae,f:=∣⟨Te,f⟩∣2.

1.1F1F5

For every e∈E the vector Te lies in K, so [F1] applied in K to the Hilbert basis F gives ∥Te∥2=∑f∈Fae,f, a supremum over finite B⊆F.

1.2F1F2

For every f∈F the vector T∗f lies in H by [F2], so [F1] applied in H to the Hilbert basis E gives ∥T∗f∥2=∑e∈E∣⟨T∗f,e⟩∣2; since ⟨T∗f,e⟩=⟨e,T∗f⟩‾ and ⟨Te,f⟩=⟨e,T∗f⟩ by [F2], the moduli agree: ∣⟨T∗f,e⟩∣=∣⟨Te,f⟩∣=ae,f1/2.

2.1step 1.1F3F4algebra

The iterated suprema agree with the rectangle supremum. For every finite A⊆E the identity sup⁡{∑e∈A∑f∈Bae,f:B⊆F finite}=∑e∈A∑f∈Fae,f holds. If A=∅, both sides are zero; hence assume A≠∅. Each row sum is the finite number ∥Te∥2 by step 1.1. The left side is at most the right side because each B gives a subsum, while for the reverse inequality fix a real η>0 and, using [F3], choose for each e∈A a finite Be⊆F with ∑f∈Beae,f>∑f∈Fae,f−η; then B:=⋃e∈ABe is finite and ∑e∈A∑f∈Bae,f≥∑e∈A∑f∈Beae,f>∑e∈A∑f∈Fae,f−∣A∣η. Hence the supremum over all finite rectangles A×B equals sup⁡A∑e∈A∑f∈Fae,f=sup⁡A∑e∈A∥Te∥2=sE(T) by [step 1.1] and [F4]; and since every finite S⊆E×F is contained in a rectangle while subsums are monotone, this rectangle supremum is also the supremum over all finite subsets of E×F.

2.2step 1.2F3F4

The same computation with the adjoint. By [step 1.2] and the same argument with E and F interchanged, sF(T∗)=sup⁡B∑f∈B∑e∈E∣⟨T∗f,e⟩∣2=sup⁡A,B∑e∈A∑f∈B∣⟨T∗f,e⟩∣2=sup⁡A,B∑e∈A∑f∈Bae,f, the last equality by the modulus identity of [step 1.2]; the middle supremum is over finite rectangles, and it is the finite-subset supremum of E×F because finite subsets of a product lie in rectangles.

3.1step 2.1step 2.2

Conclusion of the matrix-coefficient form. Steps 2.1 and 2.2 identify the rectangle supremum of claim 1 with sE(T) and with sF(T∗) respectively, so that supremum equals both sums; this proves claim 1.

4.1step 3.1

Basis independence. Let E′ be any Hilbert basis of H. Applying [step 3.1] to the pair (E′,F) gives sE′(T)=sF(T∗), and applying it to (E,F) gives sE(T)=sF(T∗) for the same basis F of K; hence sE(T)=sE′(T), and also sE(T)=sF(T∗) for every Hilbert basis F of K, both equalities holding in [0,+∞].

5.1step 4.1F6∎

Membership and the norms. By [step 4.1] the sums sE(T), sE′(T) and sF(T∗) all equal one extended real number, so they are finite simultaneously; when the common value is finite, taking nonnegative square roots gives ∥T∥HS,E=∥T∥HS,E′=∥T∗∥HS,F by [F6], and when it is +∞ none of the three norms is defined and T is Hilbert–Schmidt relative to no Hilbert basis of H. This is claim 3.

Depends on

Dependency tree · 2 levels

Sources