Approximable operators

Following Pietsch, Eigenvalues and s-numbers, §2.11. An operator S : X →L[𝕜] Y between normed 𝕜-spaces is approximable if its approximation numbers tend to zero, equivalently, if it is the operator-norm limit of a sequence of finite-rank operators.

This file develops the basic properties of the class of approximable operators:

• it is closed under addition, scalar multiplication, and pre/post-composition by bounded operators;
• it is closed in the operator-norm topology;
• every finite-rank operator is approximable;
• every approximable operator is compact (IsApproximable.isCompactOperator).

The converse direction (compact ⇒ approximable) holds on Hilbert spaces but fails for general Banach spaces (Enflo, 1973). The Hilbert-space case is treated in AddOns.Compact via the singular value decomposition.

Main definitions / results

• SVD.IsApproximable S — aₙ(S) → 0.
• SVD.isApproximable_iff_existsLimit — equivalent characterisation as a uniform limit of finite-rank operators.
• SVD.IsApproximable.isCompactOperator — every approximable operator is compact; SVD.isCompactOperator_of_rank_le specialises this to operators of finite rank.

def SVD.IsApproximable {𝕜 : Type u} [NontriviallyNormedField 𝕜] {X Y : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] (S : X →L[𝕜] Y) : Prop

An operator S : X →L[𝕜] Y is approximable if its approximation numbers tend to zero.

Equations

• SVD.IsApproximable S = Filter.Tendsto (SNumbers.approximationNumber S) Filter.atTop (nhds 0)

Equivalent characterisation

theorem SVD.isApproximable_iff_existsLimit {𝕜 : Type u} [NontriviallyNormedField 𝕜] {X Y : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] (S : X →L[𝕜] Y) : IsApproximable S ↔ ∃ (L : ℕ → X →L[𝕜] Y), (∀ (n : ℕ), (L n).rank ≤ ↑n) ∧ Filter.Tendsto (fun (n : ℕ) => ‖S - L n‖) Filter.atTop (nhds 0)

Equivalent characterisation: approximable iff a uniform limit of finite-rank operators. The forward direction extracts a near-optimal rank-≤ n approximant Lₙ with ‖S - Lₙ‖ < aₙ(S) + 1/(n+1); the converse uses approximationNumber_le_norm_sub and squeeze.

Finite-rank operators are approximable

theorem SVD.IsApproximable.of_rank_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {X Y : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {S : X →L[𝕜] Y} {N : ℕ} (hS : S.rank ≤ ↑N) : IsApproximable S

Every finite-rank continuous linear map is approximable: by (S4), aₙ(S) = 0 for all n ≥ rank S, hence aₙ(S) → 0.

Closure under linear-space operations

theorem SVD.isApproximable_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {X Y : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] : IsApproximable 0

Zero is approximable.

theorem SVD.IsApproximable.smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {X Y : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] (c : 𝕜) {S : X →L[𝕜] Y} (hS : IsApproximable S) : IsApproximable (c • S)

Scaling by a constant preserves approximability. The bound aₙ(c • S) ≤ ‖c‖ · aₙ(S) follows from the per-approximant inequality ‖c • S - c • L‖ = ‖c‖ · ‖S - L‖, taken to the infimum over rank-≤ n approximants L.

theorem SVD.IsApproximable.neg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {X Y : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {S : X →L[𝕜] Y} (hS : IsApproximable S) : IsApproximable (-S)

Negation preserves approximability, as the special case c = -1 of IsApproximable.smul.

theorem SVD.IsApproximable.add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {X Y : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {S T : X →L[𝕜] Y} (hS : IsApproximable S) (hT : IsApproximable T) : IsApproximable (S + T)

Sum of approximable operators is approximable. The proof goes through the equivalent finite-rank-limit characterisation (isApproximable_iff_existsLimit): given approximating sequences Lₘ → S and Kₘ → T, the approximant Lₙ/₂ + Kₙ₋ₙ/₂ : X →L[𝕜] Y has rank ≤ ⌊n/2⌋ + ⌈n/2⌉ = n (using LinearMap.rank_add_le) and residual ≤ ‖S - Lₙ/₂‖ + ‖T - Kₙ₋ₙ/₂‖ → 0.

Topological closure

theorem SVD.isClosed_isApproximable {𝕜 : Type u} [NontriviallyNormedField 𝕜] {X Y : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] : IsClosed {S : X →L[𝕜] Y | IsApproximable S}

Approximable operators form a closed subset of X →L[𝕜] Y.

For any S in the closure of the approximable operators and ε > 0:

• pick approximable T with ‖S - T‖ < ε/2;
• pick N with aₙ(T) < ε/2 for all n ≥ N;
• by (S2), aₙ(S) ≤ aₙ(T) + ‖S - T‖ < ε for n ≥ N.

Closure under composition

theorem SVD.IsApproximable.comp_comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {W X Y Z : Type u} [NormedAddCommGroup W] [NormedSpace 𝕜 W] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] {S : X →L[𝕜] Y} (A : W →L[𝕜] X) (B : Y →L[𝕜] Z) (hS : IsApproximable S) : IsApproximable (B ∘SL S ∘SL A)

Pre/post-composition with bounded operators preserves approximability: this is the ideal property for the class of approximable operators, inherited from the (S3) ideal property of the approximation numbers.

theorem SVD.IsApproximable.comp_left {𝕜 : Type u} [NontriviallyNormedField 𝕜] {X Y Z : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] {S : X →L[𝕜] Y} (B : Y →L[𝕜] Z) (hS : IsApproximable S) : IsApproximable (B ∘SL S)

theorem SVD.IsApproximable.comp_right {𝕜 : Type u} [NontriviallyNormedField 𝕜] {W X Y : Type u} [NormedAddCommGroup W] [NormedSpace 𝕜 W] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {S : X →L[𝕜] Y} (A : W →L[𝕜] X) (hS : IsApproximable S) : IsApproximable (S ∘SL A)

Approximable ⇒ compact

theorem SVD.IsApproximable.isCompactOperator {𝕜 : Type u} [NontriviallyNormedField 𝕜] {X Y : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [LocallyCompactSpace 𝕜] [CompleteSpace Y] {S : X →L[𝕜] Y} (hS : IsApproximable S) : IsCompactOperator ⇑S

Approximable ⇒ compact. Every operator approximable in operator norm by finite-rank ones is compact:

• a finite-rank Lₙ : X →L[𝕜] Y factors as (range Lₙ).subtypeL ∘ Lₙ' where Lₙ' : X →L[𝕜] (range Lₙ) lands in a finite-dimensional, hence locally compact, subspace; hence Lₙ is compact (isCompactOperator_of_locallyCompactSpace_dom);
• compactness is preserved under operator-norm limits (isCompactOperator_of_tendsto).

theorem SVD.isCompactOperator_of_rank_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {X Y : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [LocallyCompactSpace 𝕜] [CompleteSpace Y] {S : X →L[𝕜] Y} {m : ℕ} (hS : S.rank ≤ ↑m) : IsCompactOperator ⇑S

Finite rank ⇒ compact. An operator of rank at most m is approximable (IsApproximable.of_rank_le), hence compact.