CorollaryStatement: 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.

Finite rank operators are norm dense in compact Hilbert space operators

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ and $K$ be real or complex Hilbert spaces and let $T \in B (H, K)$ be a compact operator (Compact linear operator). Relabel the singular system of $T$ by positive integers, so its $m$ -th vectors $e_{m}, f_{m}$ correspond to the numerical singular value $s_{m} (T) > 0$ , for $1 \leq m \leq r$ in rank $r < + \infty$ and for every $m \geq 1$ in infinite rank. Let $(s_{m} (T))_{m \geq 1}$ be the zero-padded singular-value sequence (Singular value decomposition for compact operators, Absolute value and singular values of a compact operator). For $n \in N$ put $T_{n} : = \sum_{1 \leq m \leq n, s_{m} (T) > 0} s_{m} (T) ⟨ \cdot, e_{m} ⟩ f_{m},$ with the empty sum $T_{0} = 0$ . This is a finite-rank bounded operator, and $∥ T - T_{n} ∥ = s_{n + 1} (T) for every n \in N,$ so $∥ T - T_{n} ∥ \to 0$ and $T$ is the operator-norm limit of the finite-rank operators $T_{n}$ . In particular the set of finite-rank operators is norm dense in the set of compact operators $H \to K$ : every compact operator is the norm limit of finite-rank operators.

Facts & Assumptions

Given: Countable Choice, a compact $T : H \to K$ , its singular system and the truncations $T_{n}$ .

[A1]

SVD data and relabelling. The SVD supplies orthonormal singular systems indexed by the positive singular values with multiplicity, together with the norm-convergent expansion of $T$ and the corresponding partial-sum error estimate. In infinite rank its index set $N$ is order-isomorphic to the positive integers via $m \mapsto m - 1$ ; after this relabelling, and without any choice, the $m$ -th coefficient is the uniquely ordered numerical singular value $s_{m} (T)$ . Thus $T x = \sum_{m \geq 1} s_{m} (T) ⟨ x, e_{m} ⟩ f_{m}$ and $∥ T - T_{n} ∥ \leq s_{n + 1} (T)$ whenever the $(n + 1)$ -st positive singular value exists. If $r = \dim ran T < + \infty$ , then $T_{n} = T$ for $n \geq r$ and $s_{m} (T) = 0$ for $m > r$ (Singular value decomposition for compact operators, Absolute value and singular values of a compact operator).

[A2]

Finite rank. Each truncation $T_{n}$ is a finite sum of rank-one operators $⟨ \cdot, e_{j} ⟩ f_{j}$ and therefore has finite rank, hence is compact and bounded (Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis, Bounded finite rank operators are compact, A bounded linear operator between normed spaces).

[A3]

Norm test. The operator norm is the unit-ball supremum, so $∥ S ∥ \geq ∥ S x ∥$ for every unit vector $x$ and $∥ S ∥ \leq c$ follows from $∥ S x ∥ \leq c$ for all unit vectors (The operator norm as the least bound and as the unit-sphere or unit-ball supremum); limits in operator norm are metric limits (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

[A4]

Countable Choice is the standing hypothesis of this pair's Hilbert-space interface (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

Given: Countable Choice, the compact $T$ and its finite-rank truncations $T_{n}$ .

1.1

Upper bound. For every $n \in N$ : if the $(n + 1)$ -st positive singular value exists then [A1] gives $∥ T - T_{n} ∥ \leq s_{n + 1} (T)$ ; otherwise $r < + \infty$ and $n \geq r$ , so [A1] gives $T_{n} = T$ and $∥ T - T_{n} ∥ = 0 = s_{n + 1} (T)$ . This includes $T = 0$ , when $T_{n} = 0 = T$ for every $n$ . Hence $∥ T - T_{n} ∥ \leq s_{n + 1} (T)$ for every $n \in N$ .

1.2

Lower bound. Let $n \in N$ . If the $(n + 1)$ -st positive singular value exists, then $e_{n + 1}$ is a unit vector and the expansion [A1] gives $(T - T_{n}) e_{n + 1} = s_{n + 1} (T) f_{n + 1}$ , whence $∥ T - T_{n} ∥ \geq ∥ s_{n + 1} (T) f_{n + 1} ∥ = s_{n + 1} (T)$ by [A3]; otherwise $T_{n} = T$ by [A1] and $∥ T - T_{n} ∥ = 0 = s_{n + 1} (T)$ . In every case $∥ T - T_{n} ∥ \geq s_{n + 1} (T)$ .

A1A3

2.1

Conclusion. Steps 1.1 and 1.2 give $∥ T - T_{n} ∥ = s_{n + 1} (T)$ for every $n \in N$ , and $s_{n + 1} (T) \to 0$ because $(s_{m} (T))_{m \geq 1}$ is nonincreasing and nonnegative, is eventually $0$ in finite rank, and in infinite rank lists the positive eigenvalues of $∣ T ∣$ with multiplicity with only $0$ as an accumulation point [A1]; each $T_{n}$ has finite rank by [A2], so the zero-based sequence $(T_{n})_{n \in N}$ converges to $T$ in operator norm, proving the asserted density statement.

step 1.1step 1.2A1A2A3A4∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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.5, finite-rank singular truncations (printed pp. 90–93) (standard reference, not scraped)
Anthony W. Knapp, Advanced Real Analysis — Chapter II, §5 (standard reference, not scraped)