Compact operators into a Hilbert space are approximable

The last edge of the approximable/compact boundary: a compact operator whose target is a Hilbert space has aₙ(T) → 0. The other three edges are elsewhere in this directory — the characterisation of aₙ(T) → 0 as finite-rank approximability, and approximable ⇒ compact — and the four together say that on a Hilbert target, compactness is the vanishing of the approximation numbers.

• ContinuousLinearMap.exists_rank_le_natCast_norm_sub_le_of_isCompactOperator: the quantitative form — a compact operator is within ε of an operator of finite rank, for every ε > 0.
• ContinuousLinearMap.tendsto_approximationNumber_atTop_nhds_zero_of_isCompactOperator: the roadmap statement, aₙ(T) → 0.
• ContinuousLinearMap.isCompactOperator_iff_tendsto_approximationNumber: the boundary as a single equivalence, on a complete Hilbert target.

The hypothesis is on the target, not on the pair

The roadmap asks for compact operators between Hilbert spaces. What the proof uses is an orthogonal projection onto a finite-dimensional subspace of the codomain, so the domain E is an arbitrary normed space over 𝕜 and only F carries an inner product. Stating it that way is not a speculative generalisation: it is what the argument proves, and the asymmetry is the content — the counterexamples that make compact ⇒ approximable false in general are about the target's approximation property, so this is where the Hilbert hypothesis has to sit. A reader who wants the roadmap's symmetric statement gets it by instantiating E.

Completeness of F is not needed either, and is deliberately absent from the first two results: a finite-dimensional subspace of an inner-product space is complete on its own, which is what makes its orthogonal projection exist. Only the reverse implication of the final equivalence needs [CompleteSpace F], for Mathlib's closure argument.

The proof

Total boundedness, not the spectral theorem. A compact T sends the closed unit ball into a totally bounded set, so for ε > 0 finitely many ε-balls centred at points y ∈ s cover its image; let P be the orthogonal projection onto span 𝕜 s, which is finite-dimensional. For a unit vector x, the point P (T x) is the nearest point of the span to T x (Submodule.starProjection_minimal) and some y ∈ s is within ε, so ‖T x - P (T x)‖ ≤ ε; hence ‖T - P ∘L T‖ ≤ ε and P ∘L T has rank at most finrank 𝕜 (span 𝕜 s).

The spectral theorem for compact self-adjoint operators applied to T⋆T is the textbook route and was the predicted one; it proves a strictly weaker statement (it needs both spaces to be Hilbert, and F complete) through a much larger prerequisite. The nearest-point argument is recorded here because it is the one that fits the API this directory already has.

Sources

Follows nothing in particular: the finite-ε-net argument is the standard textbook proof that a Hilbert space has the approximation property, specialised to what the approximation-number API needs.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: authored directly in ForTauCeti.
• Extraction class: authored in place, for Tau Ceti.
• Original authors / copyright: Jon Crall, Claude Opus 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — imports only Mathlib and sibling staging modules.

theorem ContinuousLinearMap.exists_rank_le_natCast_norm_sub_le_of_isCompactOperator {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (hT : IsCompactOperator ⇑T) {ε : ℝ} (hε : 0 < ε) : ∃ (n : ℕ) (R : E →L[𝕜] F), (↑R).rank ≤ ↑n ∧ ‖T - R‖ ≤ ε

A compact operator into a Hilbert space is uniformly approximable by operators of finite rank. For every ε > 0 there is an R of rank at most some n with ‖T - R‖ ≤ ε.

The rank bound is delivered as R.rank ≤ (n : Cardinal) with n existentially quantified, which is the shape approximationNumber_le_norm_sub consumes; the value of n is finrank 𝕜 of the span of an ε-net of T '' closedBall 0 1, and no statement downstream depends on which n it is.

theorem ContinuousLinearMap.tendsto_approximationNumber_atTop_nhds_zero_of_isCompactOperator {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (hT : IsCompactOperator ⇑T) : Filter.Tendsto T.approximationNumber Filter.atTop (nhds 0)

A compact operator into a Hilbert space has vanishing approximation numbers. This is the roadmap's Milestone A3 and the last of the four edges of the approximable/compact boundary.

Given ε > 0, the previous theorem supplies an R of rank at most n with ‖T - R‖ ≤ ε / 2; every index m ≥ n then admits R as a competitor, so aₘ(T) ≤ ε / 2 < ε. Antitonicity of aₙ is not needed — the rank bound R.rank ≤ n ≤ m is what makes R admissible at m.

theorem ContinuousLinearMap.isCompactOperator_iff_tendsto_approximationNumber {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : IsCompactOperator ⇑T ↔ Filter.Tendsto T.approximationNumber Filter.atTop (nhds 0)

On a complete Hilbert target, compactness is the vanishing of the approximation numbers. Both implications are in this directory; the equivalence is stated because it is the boundary the roadmap describes, and reading it off the two halves requires knowing that the hypotheses line up.

[CompleteSpace F] is used only by the reverse implication, through Mathlib's closure argument for compact operators; the forward implication needs neither it nor an inner product on the domain.