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.

Hilbert–Schmidt operators are compact

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ and $K$ be real or complex Hilbert spaces (Hilbert space), let $T \in 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), let $E$ be a Hilbert basis of $H$ (Orthonormal families, complete orthonormal systems and Hilbert bases), and assume that $T$ is Hilbert–Schmidt relative to $E$ (Hilbert–Schmidt operator and Hilbert–Schmidt norm), that is, $s_{E} (T) = \sum_{e \in E} ∥ T e ∥^{2} < + \infty$ in the finite-subset-supremum convention of Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ . For finite $F \subseteq E$ let $P_{F} x : = \sum_{e \in F} ⟨ x, e ⟩ e$ be the coordinate projection (The finite Bessel inequality and best approximation by a finite orthonormal family). Then:

(finite-rank pieces) $P_{F}$ is a bounded linear operator on $H$ with $∥ P_{F} ∥ \leq 1$ , its range lies in the finite-dimensional subspace $span {e : e \in F}$ , and $T P_{F}$ is compact (Compact linear operator);
(norm estimate) $∥ T - T P_{F} ∥ \leq (\sum_{e \in E ∖ F} ∥ T e ∥^{2})^{1 / 2}$ for every finite $F \subseteq E$ , and the right-hand side is arbitrarily small for suitable finite $F$ ;
(compactness) $T$ is a compact operator.

Facts & Assumptions

Given: Countable Choice, bounded $T : H \to K$ , a Hilbert basis $E$ of $H$ with $s_{E} (T) < + \infty$ , and finite sets $F \subseteq G \subseteq E$ .

[F1]

$T$ is compact exactly when $\overline{T ({\overline{B}}_{H})}$ is a compact subset of $K$ , where ${\overline{B}}_{H} = {x \in H : ∥ x ∥ \leq 1}$ (Compact linear operator).

[F2]

For finite $F \subseteq E$ the vector $P_{F} x = \sum_{e \in F} ⟨ x, e ⟩ e$ lies in the span of ${e : e \in F}$ , $∥ P_{F} x ∥^{2} = \sum_{e \in F} ∣ ⟨ x, e ⟩ ∣^{2}$ , the residual $x - P_{F} x$ is orthogonal to every $e \in F$ , and $∥ x - P_{F} x ∥^{2} = ∥ x ∥^{2} - \sum_{e \in F} ∣ ⟨ x, e ⟩ ∣^{2} \leq ∥ x ∥^{2}$ (The finite Bessel inequality and best approximation by a finite orthonormal family).

[F3]

The finite-subset net $(P_{G} x)$ over the finite subsets $G \subseteq E$ , directed by inclusion, converges to $x$ for every $x \in H$ (Fourier expansion in a Hilbert space, Orthonormal families, complete orthonormal systems and Hilbert bases).

[F4]

Since $s_{E} (T) < + \infty$ , for every real $ε > 0$ there is a finite $F \subseteq E$ with $\sum_{e \in E ∖ F} ∥ T e ∥^{2} < ε$ ; for finite $F \subseteq G$ the finite subsum over $G ∖ F$ is at most the sum over $E ∖ F$ (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ).

[F5]

A finite set $F$ satisfies $F \approx n$ for some $n \in N$ (Finite, countably infinite, countable, uncountable); an orthonormal family is linearly independent, so the image of any enumeration of $F$ is a basis of $span {e : e \in F}$ ; a normed space that admits an ordered basis of finite length has compact closed unit ball (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, Orthonormal families, complete orthonormal systems and Hilbert bases, Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ , The closed unit ball is compact if and only if the normed space is finite-dimensional).

[F6]

A continuous image of a compact set is compact, and a closed subset of a compact metric space is compact (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact).

[F7]

A bounded linear operator is continuous, so its restriction to any normed subspace is continuous, and every $T P_{F}$ is bounded and linear (For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent, A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[F8]

A Hilbert space is a Banach space (Hilbert space, Banach space), and under Countable Choice a norm limit of compact operators into a Banach space is compact (Norm limit of compact operators is compact).

[F9]

Countable Choice allows one witness to be selected from each of countably many nonempty sets (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

Given: Countable Choice, bounded $T : H \to K$ , a Hilbert basis $E$ of $H$ with $s_{E} (T) < + \infty$ , and a finite $F \subseteq E$ .

1.1

For every $x \in H$ , [F2] gives $∥ P_{F} x ∥^{2} = \sum_{e \in F} ∣ ⟨ x, e ⟩ ∣^{2} \leq ∥ x ∥^{2}$ and $P_{F} x \in span {e : e \in F}$ ; thus $P_{F}$ is linear by construction, bounded with $∥ P_{F} ∥ \leq 1$ , and its range lies in $span {e : e \in F}$ .

F2algebra

1.2

Since $F$ is finite, [F5] fixes $n \in N$ and a bijection $σ$ from $n$ onto $F$ ; the list $e_{σ (0)}, \dots, e_{σ (n - 1)}$ is injective because the family is orthonormal, and its image spans $Z : = span {e : e \in F}$ , so it is an ordered basis of $Z$ of finite length; therefore ${\overline{B}}_{Z}$ is compact by [F5].

2.1

The set $P_{F} ({\overline{B}}_{H})$ is contained in ${\overline{B}}_{Z}$ by [step 1.1], since $∥ P_{F} x ∥ \leq ∥ x ∥ \leq 1$ and $P_{F} x \in Z$ ; the restriction of $T$ to $Z$ is continuous by [F7], so $T ({\overline{B}}_{Z})$ is compact by [step 1.2] and [F6]; as $T P_{F} ({\overline{B}}_{H}) = T (P_{F} ({\overline{B}}_{H})) \subseteq T ({\overline{B}}_{Z})$ , its closure is a closed subset of the compact set $T ({\overline{B}}_{Z})$ , hence compact by [F6], and $T P_{F}$ is compact by [F1].

step 1.1step 1.2F1F6F7

2.2

For finite $F \subseteq G \subseteq E$ and $x \in H$ we have $P_{F} P_{G} x = P_{F} x$ , because $⟨ P_{G} x, e ⟩ = ⟨ x, e ⟩$ for $e \in G$ ; hence $(I - P_{F}) P_{G} x = P_{G} x - P_{F} x = \sum_{e \in G ∖ F} ⟨ x, e ⟩ e$ and, by linearity of $T$ , $T (I - P_{F}) P_{G} x = \sum_{e \in G ∖ F} ⟨ x, e ⟩ T e$ ; the triangle inequality and the finite Cauchy–Schwarz inequality give $∥ T (I - P_{F}) P_{G} x ∥ \leq (\sum_{e \in G ∖ F} ∣ ⟨ x, e ⟩ ∣^{2})^{1 / 2} (\sum_{e \in G ∖ F} ∥ T e ∥^{2})^{1 / 2} \leq ∥ x ∥ (\sum_{e \in E ∖ F} ∥ T e ∥^{2})^{1 / 2}$ , where the last step uses [F2] for the coefficient factor and [F4] for the tail factor.

step 1.1F2F4algebra

3.1

As $G$ runs over the finite subsets of $E$ containing $F$ , the net $(I - P_{F}) P_{G} x = (P_{G} x - P_{F} x)$ converges to $(I - P_{F}) x$ , by [F3] and the boundedness of $P_{F}$ from [step 1.1]; the continuous operator $T$ of [F7] therefore carries this net to a net converging to $T (I - P_{F}) x = (T - T P_{F}) x$ , while [step 2.2] bounds every term of that net by $∥ x ∥ (\sum_{e \in E ∖ F} ∥ T e ∥^{2})^{1 / 2}$ ; the norm being continuous, the limit obeys the same bound, and taking the supremum over $∥ x ∥ \leq 1$ gives $∥ T - T P_{F} ∥ \leq (\sum_{e \in E ∖ F} ∥ T e ∥^{2})^{1 / 2}$ .

step 1.1step 2.2F3F7algebra

4.1

Given a real $ε > 0$ , [F4] provides a finite $F \subseteq E$ with $\sum_{e \in E ∖ F} ∥ T e ∥^{2} < ε^{2}$ ; then $∥ T - T P_{F} ∥ < ε$ by [step 3.1], and $T P_{F}$ is compact by [step 2.1], so for every positive tolerance there is a compact operator $T P_{F}$ within that tolerance of $T$ .

step 2.1step 3.1F4

4.2

By [F9] applied to the countably many nonempty sets of finite $F \subseteq E$ satisfying $\sum_{e \in E ∖ F} ∥ T e ∥^{2} < (n + 1)^{- 2}$ for $n \in N$ — each nonempty by [F4] — there is a sequence $(F_{n})$ of finite subsets of $E$ with these tails; then $∥ T - T P_{F_{n}} ∥ \leq (n + 1)^{- 1} \to 0$ by [step 3.1], and each $T P_{F_{n}}$ is compact by [step 2.1].

step 2.1step 3.1F4F9choose

5.1

The target $K$ is a Banach space by [F8], so the norm limit $T$ of the compact operators $T P_{F_{n}}$ is compact by [F8]; this proves claim 3, while claims 1 and 2 are [step 1.1] with [step 2.1] and [step 3.1] with [step 4.1].

step 2.1step 3.1step 4.2F8∎

Depends on

Used by

A Hilbert–Schmidt kernel operator is compact on L two Example
Finite-rank truncations of a square-integrable kernel Example
Integral operator trace under a valid diagonal hypothesis Example
Volterra operator is Hilbert Schmidt and quasinilpotent Example
Continuous convolution operators are Hilbert–Schmidt Lemma
Schatten p classes Remark
Cyclicity of the trace Theorem
Trace class iff product of two Hilbert Schmidt operators Theorem

Dependency tree · two levels

107 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, Lemma 3.23, printed pp. 93–94 (standard reference, not scraped)
John Roe, Lectures on Analysis — Lecture 13, Exercise 13.4 after Proposition 13.3, printed p. 68 (standard reference, not scraped)