Approximation numbers of bounded operators

For a bounded linear map T : E →L[𝕜] F between seminormed spaces, the n-th approximation number aₙ(T) is the distance in operator norm from T to the bounded maps of rank at most n: aₙ(T) = inf {‖T - R‖ : rank R ≤ n}. The indexing is zero-based, so a₀(T) = ‖T‖. On finite-dimensional Hilbert spaces the approximation numbers are the singular values, and in general they are the basic s-number sequence measuring how well T is approximated by finite-rank maps.

The sequence is ContinuousLinearMap.singularValue T : ℕ → ℝ≥0. This file proves its elementary calculus: the infimum characterization, antitonicity, the bound by the operator norm, the additive and multiplicative index laws a_{m+n}(S + T) ≤ aₘ(S) + aₙ(T) and a_{m+n}(S T) ≤ aₘ(S) aₙ(T), the two-sided ideal inequality aₙ(A T B) ≤ ‖A‖ aₙ(T) ‖B‖, scalar homogeneity, and Lipschitz continuity in operator norm. It also defines the Ky Fan gauge Kₖ(T) = ∑_{n<k} aₙ(T), the prefix sums from which the Ky Fan operator ideals are built.

No completeness, finite dimension, or inner product is assumed: the scalars form any nontrivially normed field and the spaces are seminormed. Spaces in different universes are allowed, so the laws apply to rectangular maps.

Main declarations

• ContinuousLinearMap.singularValue: the approximation numbers aₙ(T).
• ContinuousLinearMap.isGLB_singularValue: aₙ(T) is the infimum of ‖T - R‖ over bounded maps R of rank at most n.
• ContinuousLinearMap.singularValue_eq_zero_of_rank_le: aₙ(T) = 0 when rank T ≤ n.
• ContinuousLinearMap.singularValue_eq_zero_of_rank_domain_le: aₙ(T) = 0 when the source has rank at most n.
• ContinuousLinearMap.singularValue_zero: a₀(T) = ‖T‖.
• ContinuousLinearMap.antitone_singularValue: n ↦ aₙ(T) is antitone.
• ContinuousLinearMap.iSup_singularValue: supₙ aₙ(T) = ‖T‖.
• ContinuousLinearMap.singularValue_add_index_le: a_{m+n}(S + T) ≤ aₘ(S) + aₙ(T).
• ContinuousLinearMap.singularValue_comp_add_le_mul: a_{m+n}(S T) ≤ aₘ(S) aₙ(T).
• ContinuousLinearMap.singularValue_comp_comp_le: aₙ(A T B) ≤ ‖A‖ aₙ(T) ‖B‖.
• ContinuousLinearMap.singularValue_smul: aₙ(c T) = ‖c‖ aₙ(T).
• ContinuousLinearMap.lipschitzWith_singularValue: T ↦ aₙ(T) is 1-Lipschitz.
• ContinuousLinearMap.kyFanGauge: the Ky Fan gauge Kₖ(T) = ∑_{n<k} aₙ(T).

References

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

The approximation numbers

noncomputable def ContinuousLinearMap.singularValue {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : NNReal

The n-th approximation number aₙ(T) of a bounded linear map T: the infimum of the operator norms ‖T - R‖ over all bounded linear maps R of rank at most n. The indexing is zero-based, so a₀(T) = ‖T‖ (singularValue_zero).

On finite-dimensional Hilbert spaces these are the singular values of T.

theorem ContinuousLinearMap.singularValue_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : T.singularValue n = ⨅ (R : { R : E →L[𝕜] F // (↑R).rank ≤ ↑n }), ‖T - ↑R‖₊

aₙ(T) is the infimum of ‖T - R‖ over the bounded maps R of rank at most n.

theorem ContinuousLinearMap.singularValue_le_nnnorm_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {n : ℕ} {R : E →L[𝕜] F} (hR : (↑R).rank ≤ ↑n) : T.singularValue n ≤ ‖T - R‖₊

Approximation upper bound. Every bounded map of rank at most n bounds aₙ(T).

theorem ContinuousLinearMap.le_singularValue_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} {n : ℕ} {c : NNReal} : c ≤ T.singularValue n ↔ ∀ (R : E →L[𝕜] F), (↑R).rank ≤ ↑n → c ≤ ‖T - R‖₊

Lower-bound characterization. c ≤ aₙ(T) exactly when c ≤ ‖T - R‖ for every bounded map R of rank at most n.

theorem ContinuousLinearMap.isGLB_singularValue {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : IsGLB {x : NNReal | ∃ (R : E →L[𝕜] F), (↑R).rank ≤ ↑n ∧ ‖T - R‖₊ = x} (T.singularValue n)

Infimum formula. aₙ(T) is the greatest lower bound of the operator norms ‖T - R‖ over the bounded maps R of rank at most n.

theorem ContinuousLinearMap.exists_rank_le_nnnorm_sub_lt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} {n : ℕ} {c : NNReal} (h : T.singularValue n < c) : ∃ (R : E →L[𝕜] F), (↑R).rank ≤ ↑n ∧ ‖T - R‖₊ < c

Near-best approximants. If aₙ(T) < c, some bounded map of rank at most n lies within operator-norm distance c of T.

theorem ContinuousLinearMap.singularValue_eq_nnnorm_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {T R : E →L[𝕜] F} {n : ℕ} (hR : (↑R).rank ≤ ↑n) (hmin : ∀ (R' : E →L[𝕜] F), (↑R').rank ≤ ↑n → ‖T - R‖₊ ≤ ‖T - R'‖₊) : T.singularValue n = ‖T - R‖₊

Best approximants. A bounded map of rank at most n that is at least as close to T as every other such map attains the infimum: its distance to T is aₙ(T).

theorem ContinuousLinearMap.singularValue_le_nnnorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : T.singularValue n ≤ ‖T‖₊

The approximation numbers are bounded by the operator norm.

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

Vanishing from rank. A bounded map of rank at most n has aₙ(T) = 0.

theorem ContinuousLinearMap.singularValue_eq_zero_of_rank_domain_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {n : ℕ} (hE : Module.rank 𝕜 E ≤ ↑n) : T.singularValue n = 0

Dimension cutoff. If the source has rank at most n, then aₙ(T) = 0.

@[simp]

theorem ContinuousLinearMap.singularValue_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : T.singularValue 0 = ‖T‖₊

Zeroth approximation number. a₀(T) = ‖T‖, since only the zero map has rank 0.

theorem ContinuousLinearMap.antitone_singularValue {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : Antitone T.singularValue

The approximation numbers form an antitone sequence.

theorem ContinuousLinearMap.bddAbove_range_singularValue {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : BddAbove (Set.range T.singularValue)

The approximation numbers are bounded above by the operator norm.

@[simp]

theorem ContinuousLinearMap.iSup_singularValue {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : ⨆ (n : ℕ), T.singularValue n = ‖T‖₊

The supremum of the approximation numbers is the operator norm, attained at a₀(T).

@[simp]

theorem ContinuousLinearMap.zero_singularValue {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) : singularValue 0 n = 0

The approximation numbers of the zero map vanish.

theorem ContinuousLinearMap.singularValue_add_index_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (S T : E →L[𝕜] F) (m n : ℕ) : (S + T).singularValue (m + n) ≤ S.singularValue m + T.singularValue n

Mixed-index additive inequality. a_{m+n}(S + T) ≤ aₘ(S) + aₙ(T).

theorem ContinuousLinearMap.singularValue_add_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (S T : E →L[𝕜] F) (n : ℕ) : (S + T).singularValue n ≤ S.singularValue n + ‖T‖₊

Perturbative triangle bound. aₙ(S + T) ≤ aₙ(S) + ‖T‖.

theorem ContinuousLinearMap.abs_singularValue_sub_singularValue_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (S T : E →L[𝕜] F) (n : ℕ) : |↑(S.singularValue n) - ↑(T.singularValue n)| ≤ ‖S - T‖

Lipschitz bound at a fixed index. |aₙ(S) - aₙ(T)| ≤ ‖S - T‖.

theorem ContinuousLinearMap.lipschitzWith_singularValue {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) : LipschitzWith 1 fun (T : E →L[𝕜] F) => T.singularValue n

Lipschitz continuity. At each index, T ↦ aₙ(T) is 1-Lipschitz in operator norm.

theorem ContinuousLinearMap.continuous_singularValue {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) : Continuous fun (T : E →L[𝕜] F) => T.singularValue n

Norm continuity. At each index, T ↦ aₙ(T) is continuous in operator norm.

theorem ContinuousLinearMap.singularValue_comp_le_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (A : F →L[𝕜] G) (T : E →L[𝕜] F) (n : ℕ) : (A ∘SL T).singularValue n ≤ ‖A‖₊ * T.singularValue n

Postcomposition with a bounded map scales approximation numbers by at most its norm.

theorem ContinuousLinearMap.singularValue_comp_le_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (T : F →L[𝕜] G) (B : E →L[𝕜] F) (n : ℕ) : (T ∘SL B).singularValue n ≤ T.singularValue n * ‖B‖₊

Precomposition with a bounded map scales approximation numbers by at most its norm.

theorem ContinuousLinearMap.singularValue_comp_comp_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] (A : G →L[𝕜] H) (T : F →L[𝕜] G) (B : E →L[𝕜] F) (n : ℕ) : (A ∘SL T ∘SL B).singularValue n ≤ ‖A‖₊ * T.singularValue n * ‖B‖₊

Two-sided ideal inequality. aₙ(A T B) ≤ ‖A‖ aₙ(T) ‖B‖.

theorem ContinuousLinearMap.singularValue_comp_add_le_mul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (S : F →L[𝕜] G) (T : E →L[𝕜] F) (m n : ℕ) : (S ∘SL T).singularValue (m + n) ≤ S.singularValue m * T.singularValue n

Mixed-index product inequality. a_{m+n}(S T) ≤ aₘ(S) aₙ(T).

@[simp]

theorem ContinuousLinearMap.singularValue_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (c : 𝕜) (T : E →L[𝕜] F) (n : ℕ) : (c • T).singularValue n = ‖c‖₊ * T.singularValue n

Scalar homogeneity. aₙ(c T) = ‖c‖ aₙ(T).

The Ky Fan gauge

noncomputable def ContinuousLinearMap.kyFanGauge {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (k : ℕ) : NNReal

The Ky Fan gauge Kₖ(T) = ∑_{n<k} aₙ(T): the sum of the first k approximation numbers of T.

theorem ContinuousLinearMap.kyFanGauge_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (k : ℕ) : T.kyFanGauge k = ∑ n ∈ Finset.range k, T.singularValue n

Kₖ(T) is the sum of the approximation numbers aₙ(T) for n < k.

theorem ContinuousLinearMap.continuous_kyFanGauge {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (k : ℕ) : Continuous fun (T : E →L[𝕜] F) => T.kyFanGauge k

Each finite Ky Fan gauge is continuous for the operator norm topology.

@[simp]

theorem ContinuousLinearMap.kyFanGauge_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : T.kyFanGauge 0 = 0

The empty Ky Fan gauge vanishes.

theorem ContinuousLinearMap.kyFanGauge_succ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (k : ℕ) : T.kyFanGauge (k + 1) = T.kyFanGauge k + T.singularValue k

Each Ky Fan gauge adds the next approximation number to the previous one.

@[simp]

theorem ContinuousLinearMap.kyFanGauge_one {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : T.kyFanGauge 1 = ‖T‖₊

The first Ky Fan gauge is the operator norm: K₁(T) = ‖T‖.

theorem ContinuousLinearMap.monotone_kyFanGauge {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : Monotone T.kyFanGauge

The Ky Fan gauge is monotone in the number of summands.

theorem ContinuousLinearMap.nnnorm_le_kyFanGauge {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {k : ℕ} (hk : 0 < k) : ‖T‖₊ ≤ T.kyFanGauge k

Ky Fan lower comparison. For 0 < k, ‖T‖ ≤ Kₖ(T).

theorem ContinuousLinearMap.kyFanGauge_le_mul_nnnorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (k : ℕ) : T.kyFanGauge k ≤ ↑k * ‖T‖₊

Ky Fan upper comparison. Kₖ(T) ≤ k ‖T‖.

theorem ContinuousLinearMap.mul_singularValue_le_kyFanGauge_succ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (k : ℕ) : (↑k + 1) * T.singularValue k ≤ T.kyFanGauge (k + 1)

Ky Fan comparison with the last term. Since the approximation numbers decrease, (k + 1) aₖ(T) ≤ Kₖ₊₁(T).

@[simp]

theorem ContinuousLinearMap.kyFanGauge_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (c : 𝕜) (T : E →L[𝕜] F) (k : ℕ) : (c • T).kyFanGauge k = ‖c‖₊ * T.kyFanGauge k

Ky Fan homogeneity. Kₖ(c T) = ‖c‖ Kₖ(T).

theorem ContinuousLinearMap.kyFanGauge_comp_comp_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] (A : G →L[𝕜] H) (T : F →L[𝕜] G) (B : E →L[𝕜] F) (k : ℕ) : (A ∘SL T ∘SL B).kyFanGauge k ≤ ‖A‖₊ * T.kyFanGauge k * ‖B‖₊

Ky Fan two-sided ideal inequality. Kₖ(A T B) ≤ ‖A‖ Kₖ(T) ‖B‖.