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.

Compact operator iff approximation numbers tend to zero

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 bounded linear operator (A bounded linear operator between normed spaces, Hilbert space). Put $a_{0} (T) : = ∥ T ∥$ , and for $n \geq 1$ put $a_{n} (T) : = \inf {∥ T - F ∥ : F \in B (H, K), \dim ran F < n}$ (Greatest lower bound (infimum), The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis), where only finite-rank $F$ are admitted. The error set contains $∥ T ∥$ by taking $F = 0$ and is bounded below by $0$ , so its real infimum exists by Every nonempty set bounded below has an infimum. Thus $(a_{n} (T))_{n \in N}$ is a sequence in the library's zero-based convention. Then $T$ is compact (Compact linear operator) if and only if $a_{n} (T) \to 0$ (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ). If $T$ is compact, then $a_{n} (T) = s_{n} (T)$ for every $n$ , where $(s_{n} (T))$ is the zero-padded singular-value sequence of $T$ (Absolute value and singular values of a compact operator) for every $n \geq 1$ .

Facts & Assumptions

Given: Countable Choice, Hilbert spaces $H, K$ , a bounded $T \in B (H, K)$ and the approximation numbers $a_{n} (T)$ .

[A1]

Compact case. If $T$ is compact then $a_{n} (T) = s_{n} (T)$ for all $n$ , and $s_{n} (T) \to 0$ : the sequence $(s_{n} (T))$ is nonincreasing with nonnegative terms, is eventually $0$ in the finite-rank case, and in the infinite-rank case consists of the positive eigenvalues of $∣ T ∣$ listed with multiplicity, which by the spectral theorem have only $0$ as accumulation point, so the nonincreasing listing tends to $0$ (Singular values equal approximation numbers, Absolute value and singular values of a compact operator, Singular value decomposition for compact operators).

[A2]

Finite-rank operators are compact. A bounded finite-rank operator is compact; a norm limit of compact operators with Banach target is compact under ${A C}_{ω}$ ; a Hilbert space is a Banach space (Bounded finite rank operators are compact, Norm limit of compact operators is compact, Hilbert space, Banach space).

[A3]

Infimum and convergence. Every nonempty bounded-below set of reals has a real infimum (Every nonempty set bounded below has an infimum). Each defining error set is nonempty because it contains the error of $F = 0$ , and is bounded below by $0$ . For every real $ε > 0$ it has an element $x < \inf + ε$ : otherwise $\inf + ε$ would be a larger lower bound, contradicting the greatest-lower-bound definition; a sequence of real numbers tends to $0$ when for every $ε > 0$ eventually $∣ a_{n} ∣ < ε$ (Greatest lower bound (infimum), Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

[A4]

Countable Choice selects one finite-rank approximant for each $n \geq 1$ by applying it to the shifted family indexed by $N$ ; assigning $F_{0} = 0$ then gives a zero-based sequence (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

Given: Countable Choice, the Hilbert spaces $H, K$ , the bounded operator $T$ , and the numbers $a_{n} (T)$ .

1.1

Compact implies vanishing. If $T$ is compact then [A1] gives $a_{n} (T) = s_{n} (T)$ for all $n \geq 1$ and $s_{n} (T) \to 0$ along the positive-indexed tail, so the zero-based sequence $(a_{n} (T))_{n \in N}$ tends to $0$ ; its single value $a_{0} (T) = ∥ T ∥$ does not affect convergence.

1.2

Vanishing implies compact. Assume $(a_{n} (T))_{n \in N} \to 0$ . Since the infimum defining $a_{n} (T)$ is over a nonempty set, for each $n \geq 1$ there is $F_{n} \in B (H, K)$ with $\dim ran F_{n} < n$ and $∥ T - F_{n} ∥ < a_{n} (T) + 1 / n$ , by [A3]; countable choice [A4] selects these operators, and we put $F_{0} = 0$ to obtain a sequence indexed by $N$ . Each $F_{n}$ has finite rank, hence is compact, and $∥ T - F_{n} ∥ \to 0$ because the tail satisfies $0 \leq ∥ T - F_{n} ∥ < a_{n} (T) + 1 / n \to 0$ ; as the target $K$ is a Banach space, [A2] makes $T$ compact.

A2A3A4algebra

2.1

Conclusion. Steps 1.1 and 1.2 give the equivalence; the identification $a_{n} (T) = s_{n} (T)$ in the compact case for every $n \geq 1$ is [A1].

step 1.1step 1.2A1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

86 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, Lemma 3.19 and its converse (printed pp. 92–93) (standard reference, not scraped)
Anthony W. Knapp, Advanced Real Analysis — Chapter II, §5 (standard reference, not scraped)