Approximation numbers of bounded operators

The zero-based approximation number of a continuous linear map T at index n is the operator-norm distance from T to continuous linear maps of rank at most n. This file develops its elementary order and ideal API over an arbitrary nontrivially normed field, with independent source and target universes.

The declarations here deliberately stop before Hilbert-space-specific results: adjoint invariance, finite-dimensional singular-value identification, and infinite-dimensional min--max lower bounds live in sibling modules.

The index convention

The operator-ideal literature is split. Pietsch's s-numbers are one-based, sₙ(T) = dist(T, {rank < n}) with s₁(T) = ‖T‖; here aₙ(T) is zero-based, aₙ(T) = dist(T, {rank ≤ n}) with a₀(T) = ‖T‖, so sₙ = a_{n-1}. Only one of the two is developed — carrying both would duplicate the whole API for an index shift — and the zero-based one is chosen because every downstream statement is off-by-one free in it:

• the additive ideal inequality is a_{m+n}(S + T) ≤ aₘ(S) + aₙ(T) (ContinuousLinearMap.approximationNumber_add_le), against the one-based s_{m+n-1};
• the singular-value identification is aₙ(T) = σₙ(T) (ContinuousLinearMap.approximationNumber_eq_singularValues), a genuine identity of indices, because Mathlib's LinearMap.singularValues is itself zero-indexed; one-based numbering would put an n - 1 — truncated subtraction — into the flagship theorem of the development;
• a₀(T) = ‖T‖ needs no convention at n = 0, whereas the one-based s₀ has to be defined by fiat.

The convention is stated in the first sentence of the definition's docstring and is recorded as decision 1 of TauCetiRoadmap/OperatorTheory/OperatorIdeals/README.md (Part A generality bar).

Main declarations

• ContinuousLinearMap.approximationNumber: the nth zero-based approximation number, valued in ℝ.
• ContinuousLinearMap.approximationNumber_le_norm_sub and ContinuousLinearMap.le_approximationNumber_iff: the characteristic upper and lower bounds. Together they replace unfolding the definition; the defining infimum itself is available as ContinuousLinearMap.approximationNumber_eq_iInf, which is deliberately not a simp lemma.
• ContinuousLinearMap.approximationNumber_index_zero: the zeroth approximation number is the operator norm. The index, not the operator, is what is zero here; ContinuousLinearMap.approximationNumber_zero is the companion statement about the zero operator, matching Mathlib's LinearMap.singularValues_zero.
• ContinuousLinearMap.approximationNumber_antitone: approximation numbers decrease with the allowed rank.
• ContinuousLinearMap.approximationNumber_add_le, approximationNumber_comp_le_norm_mul, approximationNumber_comp_le_mul_norm, approximationNumber_comp_comp_le: the additive and two-sided ideal inequalities.
• ContinuousLinearMap.approximationNumber_comp_eq_of_leftInverse: enlarging the codomain along a contraction with a contractive left inverse changes nothing.
• ContinuousLinearMap.approximationNumber_smul: absolute homogeneity.

Namespace note

These declarations extend the existing Mathlib namespace ContinuousLinearMap rather than living under TauCeti, so that dot notation (T.approximationNumber) resolves and the names match the eventual Mathlib upstreaming target (adapted from Mathlib PR #32126). Lean field projection binds T.approximationNumber only to the literal ContinuousLinearMap.approximationNumber and does not consult the enclosing TauCeti namespace. This is a deliberate API choice, flagged for Tau Ceti maintainer review.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib/Analysis/Normed/Operator/ApproximationNumber.lean at Davis--Kahan commit fc38eb48b9b49f2e1d87fe0c7022dc5e262820a7.
• Original declarations: ContinuousLinearMap.approximationNumber and the order and ideal API in the same namespace, plus two pieces of plumbing that have since moved out so that this module carries approximation-number API and nothing else: the universe helper Cardinal.le_natCast_of_lift_le (now the iff Cardinal.lift_le_natCast in ForTauCeti/SetTheory/Cardinal/Lift.lean) and the rank-of-composition bounds rank_comp_left_le_of_rank_le and rank_comp_right_le_rank (now ContinuousLinearMap.rank_comp_le_natCast_right and ContinuousLinearMap.rank_comp_le_left in ForTauCeti/LinearAlgebra/Dimension/RankComp.lean, generalized to LinearMap).
• Original authors / copyright: Jon Crall, OpenAI GPT-5.6 Thinking, Niels Voss, Arnav Mehta, Rawad Kansoh; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• The Davis--Kahan file was itself adapted from Mathlib PR #32126.
• Extraction class: copied, converted to the Tau Ceti module system, then renamed conclusion-outward per the signature-polish backlog No mathematical change; see Appendix A of that document for the name index.
• Spectra influence: none — this module has no Spectra dependency and never did; it imports only Mathlib.

noncomputable def ContinuousLinearMap.approximationNumber {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : ℝ

The zero-based approximation number aₙ(T): the operator-norm distance from T to the continuous linear maps of rank at most n.

The indexing is zero-based, so a₀(T) = ‖T‖ (ContinuousLinearMap.approximationNumber_index_zero). This differs from the one-based convention sₙ(T) = dist(T, {rank < n}) common in the operator-ideal literature (Pietsch), for which s₁(T) = ‖T‖; the translation is sₙ = a_{n-1}. The zero-based form is the one used throughout this development: see the module docstring for why.

Equations

• T.approximationNumber n = ⨅ (R : { R : E →L[𝕜] F // (↑R).rank ≤ ↑n }), ‖T - ↑R‖

theorem ContinuousLinearMap.approximationNumber_eq_iInf {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : T.approximationNumber n = ⨅ (R : { R : E →L[𝕜] F // (↑R).rank ≤ ↑n }), ‖T - ↑R‖

The defining infimum. Stated for proofs that genuinely need the construction; it is deliberately not a simp lemma, since a ciInf over a subtype is not a useful normal form for a norm-like quantity. Prefer ContinuousLinearMap.approximationNumber_le_norm_sub and ContinuousLinearMap.le_approximationNumber_iff.

theorem ContinuousLinearMap.approximationNumber_le_norm_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {n : ℕ} {R : E →L[𝕜] F} (hR : (↑R).rank ≤ ↑n) : T.approximationNumber n ≤ ‖T - R‖

Every admissible approximation of rank at most n bounds aₙ(T) above.

theorem ContinuousLinearMap.le_approximationNumber_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {n : ℕ} {x : ℝ} : x ≤ T.approximationNumber n ↔ ∀ (R : E →L[𝕜] F), (↑R).rank ≤ ↑n → x ≤ ‖T - R‖

Characteristic lower-bound property: x bounds aₙ(T) from below exactly when it bounds every admissible approximation error.

theorem ContinuousLinearMap.approximationNumber_eq_norm_sub_of_forall_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {n : ℕ} {R : E →L[𝕜] F} (hR : (↑R).rank ≤ ↑n) (hbest : ∀ (S : E →L[𝕜] F), (↑S).rank ≤ ↑n → ‖T - R‖ ≤ ‖T - S‖) : T.approximationNumber n = ‖T - R‖

A best approximation of rank at most n computes aₙ(T): if no admissible S does better than R, then the infimum is attained at R.

Existence of such an R is not automatic — the defining infimum need not be attained — which is why this is stated with the minimality hypothesis rather than as an unconditional ∃.

@[simp]

theorem ContinuousLinearMap.approximationNumber_index_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : T.approximationNumber 0 = ‖T‖

The zeroth approximation number is the operator norm: allowing rank-0 approximants allows only 0. This is the statement that fixes the zero-based convention; see the module docstring. Not to be confused with ContinuousLinearMap.approximationNumber_zero, which is about the zero operator.

theorem ContinuousLinearMap.approximationNumber_antitone {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : Antitone T.approximationNumber

Approximation numbers decrease with the allowed rank.

theorem ContinuousLinearMap.approximationNumber_le_norm {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : T.approximationNumber n ≤ ‖T‖

Every approximation number is bounded by the operator norm.

theorem ContinuousLinearMap.approximationNumber_nonneg {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : 0 ≤ T.approximationNumber n

Approximation numbers are nonnegative. (With the real-valued codomain this is a theorem rather than a triviality; it is the price of matching the Mathlib convention for norm-like quantities.)

@[simp]

theorem ContinuousLinearMap.approximationNumber_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) : approximationNumber 0 n = 0

The zero operator has every approximation number equal to zero. Named for the operator, as in Mathlib's LinearMap.singularValues_zero; the companion ContinuousLinearMap.approximationNumber_index_zero is the one about index 0.

theorem ContinuousLinearMap.approximationNumber_eq_zero_of_rank_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {n : ℕ} (hT : (↑T).rank ≤ ↑n) : T.approximationNumber n = 0

The rank cutoff. An operator of rank at most n is its own best approximation of rank at most n, so aₙ(T) = 0.

This is the first of the four statements roadmap topic T09 §A4 asks for. It holds over any normed pair — no inner product, no completeness, no finite dimension — because R := T is admissible in the defining infimum. The converse for a finite-dimensional source over a complete field is proved in ApproximationNumber.Rank as approximationNumber_eq_zero_iff_rank_le; it does not require an inner product.

theorem ContinuousLinearMap.approximationNumber_eq_zero_of_rank_le_of_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {r n : ℕ} (hT : (↑T).rank ≤ ↑r) (hrn : r ≤ n) : T.approximationNumber n = 0

Every approximation number at or past the rank vanishes: the cutoff ContinuousLinearMap.approximationNumber_eq_zero_of_rank_le in the form a consumer with a finite rank bound uses.

theorem ContinuousLinearMap.exists_rank_le_norm_sub_lt_approximationNumber_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (R : E →L[𝕜] F), (↑R).rank ≤ ↑n ∧ ‖T - R‖ < T.approximationNumber n + ε

Near-minimizers exist: the defining infimum is approached to within any ε > 0 by an admissible approximant. This is the workhorse behind every inequality below, each of which builds an approximant for the left-hand side out of near-minimizers for the right.

theorem ContinuousLinearMap.approximationNumber_add_le_add_norm {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T S : E →L[𝕜] F) (n : ℕ) : (T + S).approximationNumber n ≤ T.approximationNumber n + ‖S‖

Approximation numbers are 1-Lipschitz in the ambient operator norm. The index-shifted ContinuousLinearMap.approximationNumber_add_le is the sharper statement; this is its n = 0 specialization in the second summand, kept separate because perturbation arguments want the norm on the right.

theorem ContinuousLinearMap.abs_approximationNumber_sub_approximationNumber_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T S : E →L[𝕜] F) (n : ℕ) : |T.approximationNumber n - S.approximationNumber n| ≤ ‖T - S‖

Each approximation number is 1-Lipschitz in the operator norm: |aₙ(T) − aₙ(S)| ≤ ‖T − S‖.

This is the reverse-triangle form of approximationNumber_add_le_add_norm, and it is the perturbation statement downstream arguments actually want: it says the whole s-sequence moves no faster than the operator does. In finite dimensions it specializes to Weyl's inequality for singular values, via approximationNumber_eq_singularValues.

theorem ContinuousLinearMap.approximationNumber_add_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T S : E →L[𝕜] F) (m n : ℕ) : (T + S).approximationNumber (m + n) ≤ T.approximationNumber m + S.approximationNumber n

The additive ideal inequality: a_{m+n}(T + S) ≤ aₘ(T) + aₙ(S), because two approximants of ranks at most m and n add to one of rank at most m + n. The index shift is exact in the zero-based convention — one-based s-numbers would carry an m + n - 1 here.

theorem ContinuousLinearMap.approximationNumber_comp_add_le_mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type x} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (S : F →L[𝕜] G) (T : E →L[𝕜] F) (m n : ℕ) : (S ∘SL T).approximationNumber (m + n) ≤ S.approximationNumber m * T.approximationNumber n

Composition multiplicativity across indices: a_{m+n}(S ∘ T) ≤ aₘ(S) · aₙ(T).

The name carries add deliberately. approximationNumber_comp_comp_le is the two-sided ideal bound aₙ(L ∘ T ∘ R) ≤ ‖L‖ · aₙ(T) · ‖R‖, a different theorem at a fixed index; this one splits the index, which is what makes the approximation numbers behave like a multiplicative scale and is the input to the Schatten Hölder inequalities.

The approximant is R₁ ∘ T + (S - R₁) ∘ R₂, whose rank is at most m + n because each summand is bounded by the rank of its own finite-rank factor — the left one by R₁, the right one by R₂. The residual then factors as (S - R₁) ∘ (T - R₂), so the two approximation errors multiply.

theorem ContinuousLinearMap.approximationNumber_comp_le_mul_norm {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type x} [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (T : E →L[𝕜] F) (A : G →L[𝕜] E) (n : ℕ) : (T ∘SL A).approximationNumber n ≤ T.approximationNumber n * ‖A‖

Right ideal inequality for approximation numbers.

theorem ContinuousLinearMap.approximationNumber_comp_le_norm_mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type x} [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (B : F →L[𝕜] G) (T : E →L[𝕜] F) (n : ℕ) : (B ∘SL T).approximationNumber n ≤ ‖B‖ * T.approximationNumber n

Left ideal inequality for approximation numbers.

theorem ContinuousLinearMap.approximationNumber_comp_comp_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type x} {H : Type y} [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup H] [NormedSpace 𝕜 H] (L : F →L[𝕜] G) (T : E →L[𝕜] F) (R : H →L[𝕜] E) (n : ℕ) : (L ∘SL T ∘SL R).approximationNumber n ≤ ‖L‖ * T.approximationNumber n * ‖R‖

Two-sided ideal inequality for approximation numbers.

theorem ContinuousLinearMap.approximationNumber_comp_eq_of_leftInverse {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type x} [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {ι : F →L[𝕜] G} {π : G →L[𝕜] F} (hπι : Function.LeftInverse ⇑π ⇑ι) (hι : ‖ι‖ ≤ 1) (hπ : ‖π‖ ≤ 1) (T : E →L[𝕜] F) (n : ℕ) : (ι ∘SL T).approximationNumber n = T.approximationNumber n

Approximation numbers do not see an enlargement of the codomain.

ι embeds F into G with ‖ι‖ ≤ 1, and π is a left inverse with ‖π‖ ≤ 1; the model is the inclusion of F as one summand of an ℓ² direct sum together with the projection back onto it. Postcomposing with ι then leaves every approximation number where it was, because both ideal inequalities apply and π ∘ ι = id closes the loop. (The two hypotheses force ι to be isometric: ‖y‖ = ‖π (ι y)‖ ≤ ‖ι y‖ ≤ ‖y‖.)

Nothing here needs an inner product, completeness, or a bound on any dimension. Its use is to move an operator into a codomain with room for as many orthonormal vectors as an argument needs, without changing the quantity being computed.

@[simp]

theorem ContinuousLinearMap.approximationNumber_smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (c : 𝕜) (T : E →L[𝕜] F) (n : ℕ) : (c • T).approximationNumber n = ‖c‖ * T.approximationNumber n

Approximation numbers are absolutely homogeneous.