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 ()). Let , and be real or complex Hilbert spaces and let be a Hilbert basis of (supplied as data), with the Hilbert–Schmidt square-sum and the Hilbert–Schmidt norm of Hilbert–Schmidt operator and Hilbert–Schmidt norm. Then:
- if are Hilbert–Schmidt relative to , then so is for all scalars , and
- if is Hilbert–Schmidt relative to , then for every Hilbert basis of the adjoint is Hilbert–Schmidt relative to and
- if is Hilbert–Schmidt relative to and , are bounded with a Hilbert basis of and a supplied Hilbert basis of , then is Hilbert–Schmidt relative to and is Hilbert–Schmidt relative to , with and consequently
Facts & Assumptions
Given: Countable Choice, real or complex Hilbert spaces , a Hilbert basis of , Hilbert–Schmidt operators relative to , and bounded operators , .
For claim 3, Hilbert bases of and of are supplied as additional data; their existence is not inferred from Countable Choice.
Hilbert–Schmidt data. For a Hilbert basis of , is the supremum of the finite subsums, is Hilbert–Schmidt relative to when , and then ; the finite-subset supremum splits as for finite (Hilbert–Schmidt operator and Hilbert–Schmidt norm, Square-summable families on an arbitrary index set and the space ).
Adjoint invariance. For every Hilbert basis of and of one has , and membership and norms agree across all such bases (The Hilbert–Schmidt norm is basis independent, Hilbert space).
Bounds. and for bounded operators, and (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).
Minkowski in finite dimension. For finitely many vectors of an inner-product space, ; for finitely many pairs of nonnegative reals the Cauchy–Schwarz inequality gives (Cauchy–Schwarz: , with equality exactly for dependent pairs, Real and complex inner-product spaces and their induced length).
Proof
Given: Countable Choice, the Hilbert spaces and bases above, Hilbert–Schmidt relative to , and bounded .
Vector space. For every finite , [A3] and [A5] give , so the finite subsums for are bounded by the square of the last quantity [A1] and is Hilbert–Schmidt relative to with the asserted norm bound.
Adjoint. For every Hilbert basis of , by [A2], so is Hilbert–Schmidt relative to and .
Left multiplication. For finite , [A3] gives , so is Hilbert–Schmidt relative to with .
Right multiplication. Let and be the supplied Hilbert bases of and , respectively, and put , so by [A3]. By [step 1.2], is Hilbert–Schmidt relative to , and [step 1.3] applied to the left multiplication gives that is Hilbert–Schmidt relative to with Now apply [step 1.2] to the Hilbert–Schmidt operator , using as its domain basis and as its codomain basis. It follows that is Hilbert–Schmidt relative to and has Hilbert–Schmidt norm . Since by [A3], is Hilbert–Schmidt relative to and
Both-sided bound. Combining [step 1.3] with in place of and [step 2.1], is Hilbert–Schmidt relative to with .
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 , and are supplied as data and only the finite-subset supremum definition of [A1] and the invariance theorem [A2] are used.
Depends on
- Hilbert–Schmidt operator and Hilbert–Schmidt norm
- The Hilbert–Schmidt norm is basis independent
- Hilbert-adjoint identities
- The Hilbert-space adjoint of a bounded operator
- Cauchy–Schwarz: $|\langle x,y\rangle|\le\|x\|\,\|y\|$, with equality exactly for dependent pairs
- 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 $\ell^2(I)$
- Orthonormal families, complete orthonormal systems and Hilbert bases
- Real and complex inner-product spaces and their induced length
- Hilbert space
- 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\|
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
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
- Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §3.6, Lemmas 3.23–3.25 (printed pp. 93–97) (standard reference, not scraped)
- Anthony W. Knapp, Advanced Real Analysis — Chapter II, §5, Proposition 2.8 (standard reference, not scraped)