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.

Hilbert Schmidt operators form a two sided ideal

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let H, K and L be real or complex Hilbert spaces and let E be a Hilbert basis of H (supplied as data), with sE(T)=eETe2 the Hilbert–Schmidt square-sum and THS,E the Hilbert–Schmidt norm of Hilbert–Schmidt operator and Hilbert–Schmidt norm. Then:

  1. if S,TB(H,K) are Hilbert–Schmidt relative to E, then so is aS+bT for all scalars a,b, and aS+bTHS,EaSHS,E+bTHS,E;
  2. if TB(H,K) is Hilbert–Schmidt relative to E, then for every Hilbert basis F of K the adjoint T is Hilbert–Schmidt relative to F and THS,F=THS,E;
  3. if TB(H,K) is Hilbert–Schmidt relative to E and AB(K,L), BB(H0,H) are bounded with E0 a Hilbert basis of H0 and F a supplied Hilbert basis of K, then ATB(H,L) is Hilbert–Schmidt relative to E and TBB(H0,K) is Hilbert–Schmidt relative to E0, with ATHS,EATHS,E,TBHS,E0THS,EB, and consequently ATBHS,E0ATHS,EB.

Facts & Assumptions

Given: Countable Choice, real or complex Hilbert spaces H,H0,K,L, a Hilbert basis E of H, Hilbert–Schmidt operators S,T relative to E, and bounded operators AB(K,L), BB(H0,H).

For claim 3, Hilbert bases E0 of H0 and F of K are supplied as additional data; their existence is not inferred from Countable Choice.

[A1]

Hilbert–Schmidt data. For a Hilbert basis E of H, sE(T)=eETe2 is the supremum of the finite subsums, T is Hilbert–Schmidt relative to E when sE(T)<+, and then THS,E=sE(T)1/2; the finite-subset supremum splits as eETe2=eFTe2+eEFTe2 for finite F (Hilbert–Schmidt operator and Hilbert–Schmidt norm, Square-summable families on an arbitrary index set and the space 2(I)).

[A2]

Adjoint invariance. For every Hilbert basis E of H and F of K one has sE(T)=sE(T)=sF(T), and membership and norms agree across all such bases (The Hilbert–Schmidt norm is basis independent, Hilbert space).

[A3]

Bounds. SvSv and UVUV for bounded operators, and B=B (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, A bounded linear operator between normed spaces, Composition satisfies |ST|\le|S|,|T|, Hilbert-adjoint identities).

[A5]

Minkowski in finite dimension. For finitely many vectors v1,,vm of an inner-product space, kvkkvk; for finitely many pairs of nonnegative reals the Cauchy–Schwarz inequality gives (k(ak+bk)2)1/2(kak2)1/2+(kbk2)1/2 (Cauchy–Schwarz: x,yxy, with equality exactly for dependent pairs, Real and complex inner-product spaces and their induced length).

Proof

technique · direct

Given: Countable Choice, the Hilbert spaces and bases above, Hilbert–Schmidt S,T relative to E, and bounded A,B.

1.1

Vector space. For every finite FE, [A3] and [A5] give (eF(aS+bT)e2)1/2a(FSe2)1/2+b(FTe2)1/2aSHS,E+bTHS,E, so the finite subsums for aS+bT are bounded by the square of the last quantity [A1] and aS+bT is Hilbert–Schmidt relative to E with the asserted norm bound.

A1A3A5algebra
1.2

Adjoint. For every Hilbert basis F of K, sF(T)=sE(T) by [A2], so T is Hilbert–Schmidt relative to F and THS,F=THS,E.

A1A2
1.3

Left multiplication. For finite FE, [A3] gives eFATe2A2eFTe2A2THS,E2, so AT is Hilbert–Schmidt relative to E with ATHS,EATHS,E.

A1A3algebra
2.1

Right multiplication. Let E0 and F be the supplied Hilbert bases of H0 and K, respectively, and put U:=TBB(H0,K), so U=BT by [A3]. By [step 1.2], T is Hilbert–Schmidt relative to F, and [step 1.3] applied to the left multiplication BT gives that U is Hilbert–Schmidt relative to F with UHS,FBTHS,F=BTHS,E. Now apply [step 1.2] to the Hilbert–Schmidt operator U:KH0, using F as its domain basis and E0 as its codomain basis. It follows that (U)=U is Hilbert–Schmidt relative to E0 and has Hilbert–Schmidt norm UHS,F. Since U=U by [A3], U=TB is Hilbert–Schmidt relative to E0 and TBHS,E0=UHS,FTHS,EB.

step 1.2step 1.3A2A3
3.1

Both-sided bound. Combining [step 1.3] with TB in place of T and [step 2.1], ATB=(AT)B is Hilbert–Schmidt relative to E0 with ATBHS,E0ATBHS,E0ATHS,EB.

step 1.3step 2.1
4.1

Conclusion. Claim 1 is [step 1.1], claim 2 is [step 1.2] and claim 3 is the combination of [step 1.3], [step 2.1] and [step 3.1]; no Hilbert basis is assumed to exist, since E, E0 and F are supplied as data and only the finite-subset supremum definition of [A1] and the invariance theorem [A2] are used.

step 1.1step 1.2step 1.3step 2.1step 3.1A2

Depends on

Used by

Dependency tree · two levels

62 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