Approximation numbers, rank, and compactness

The approximation numbers aₙ(T) of a bounded linear map T : E →L[𝕜] F measure its distance to the maps of rank at most n. This file relates their vanishing and their decay to rank, finite-rank approximability and compactness.

• Over a complete field, aₙ(T) = 0 exactly when rank T ≤ n. The maps of rank greater than n form an open set, so a limit of maps of rank at most n again has rank at most n. No finite dimension is needed.
• aₙ(T) → 0 exactly when T is the operator-norm limit of a sequence (Rₙ) with rank Rₙ ≤ n.
• Over a locally compact field and with a complete target, such a limit is a compact operator.
• Conversely, a compact operator into an inner product space satisfies aₙ(T) → 0: the image of the unit ball is covered by finitely many ε-balls, and composing T with the orthogonal projection onto the span of their centres gives a finite-rank map within ε of T. The target need not be complete.

Combining the two directions, a bounded operator into a Hilbert space is compact exactly when its approximation numbers tend to zero.

Main declarations

• ContinuousLinearMap.singularValue_eq_zero_iff_rank_le: aₙ(T) = 0 ↔ rank T ≤ n.
• ContinuousLinearMap.tendsto_singularValue_nhds_zero_iff: aₙ(T) → 0 exactly when T is a limit of maps Rₙ with rank Rₙ ≤ n.
• ContinuousLinearMap.isCompactOperator_of_tendsto_singularValue: if aₙ(T) → 0 and the target is complete, T is compact.
• IsCompactOperator.tendsto_singularValue: a compact operator into an inner product space has aₙ(T) → 0.
• ContinuousLinearMap.isCompactOperator_iff_tendsto_singularValue: an operator into a Hilbert space is compact exactly when aₙ(T) → 0.

References

• A. Pietsch, Eigenvalues and s-Numbers, Cambridge Studies in Advanced Mathematics 13, Cambridge University Press (1987), §2.2.
• I. C. Gohberg, M. G. Krein, Introduction to the Theory of Linear Nonselfadjoint Operators, Translations of Mathematical Monographs 18, AMS (1969), Chapter II, §2.

theorem ContinuousLinearMap.tendsto_singularValue_nhds_zero_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} : Filter.Tendsto T.singularValue Filter.atTop (nhds 0) ↔ ∃ (R : ℕ → E →L[𝕜] F), (∀ (n : ℕ), (↑(R n)).rank ≤ ↑n) ∧ Filter.Tendsto R Filter.atTop (nhds T)

Finite-rank approximation. The approximation numbers of T tend to zero exactly when T is the operator-norm limit of a sequence of bounded maps Rₙ with rank Rₙ ≤ n.

theorem ContinuousLinearMap.singularValue_eq_zero_iff_rank_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} {n : ℕ} : T.singularValue n = 0 ↔ (↑T).rank ≤ ↑n

Rank characterization. Over a complete field, aₙ(T) = 0 exactly when rank T ≤ n: a map approximated arbitrarily well by maps of rank at most n has rank at most n itself.

theorem ContinuousLinearMap.isCompactOperator_of_tendsto_singularValue {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F} (h : Filter.Tendsto T.singularValue Filter.atTop (nhds 0)) : IsCompactOperator ⇑T

Approximability implies compactness. Over a locally compact field, a bounded map into a Banach space whose approximation numbers tend to zero is a compact operator.

theorem IsCompactOperator.tendsto_singularValue {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →L[𝕜] F} (hT : IsCompactOperator ⇑T) : Filter.Tendsto T.singularValue Filter.atTop (nhds 0)

Compactness implies approximability on an inner product space target. The approximation numbers of a compact operator into an inner product space tend to zero. The target need not be complete.

theorem ContinuousLinearMap.isCompactOperator_iff_tendsto_singularValue {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F} : IsCompactOperator ⇑T ↔ Filter.Tendsto T.singularValue Filter.atTop (nhds 0)

Compactness characterization on a Hilbert space target. A bounded operator into a Hilbert space is compact exactly when its approximation numbers tend to zero.