Approximation numbers on finite-dimensional Hilbert spaces

This module begins the bridge between the finite-dimensional singular-value library and approximation numbers defined by finite-rank operator-norm approximation.

The main result is the finite-dimensional Eckart--Young identification: the nth approximation number equals the nth singular value. The lower bound uses the Courant--Fischer (n+1)-dimensional right singular subspace and dimension counting against the kernel of an arbitrary rank-at-most-n approximant. The upper bound projects onto the first n right singular directions and controls the complementary spectral tail.

Main declarations

• ContinuousLinearMap.approximationNumber_eq_singularValues: the identification aₙ(T) = σₙ(T), index for index — the whole point of the zero-based convention (see ApproximationNumber/Basic.lean).
• ContinuousLinearMap.singularValues_le_norm_sub_of_rank_le: the sharp lower bound against an arbitrary rank-at-most-n approximant. It is strictly stronger than the inequality below, which is its infimum form.
• ContinuousLinearMap.singularValues_le_approximationNumber: the half of the identification that does not depend on the truncation construction, and so the half that has a shape in infinite dimensions.

The reverse inequality is private: it is the half that exists only to be combined into the identification. See the declaration for the reasoning.

Namespace note

These declarations extend the existing Mathlib namespace ContinuousLinearMap rather than living under TauCeti, so that dot notation (T.approximationNumber_eq_singularValues) resolves and the names match the eventual Mathlib upstreaming target. Lean field projection binds T.foo only to the literal ContinuousLinearMap.foo and does not consult the enclosing TauCeti namespace. The Courant--Fischer helpers imported here, by contrast, live under TauCeti. 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/ApproximationNumberSingularValues.lean at Davis--Kahan commit fc38eb48b9b49f2e1d87fe0c7022dc5e262820a7.
• Original declarations: ContinuousLinearMap.approximationNumber_eq_singularValues and the Eckart--Young bounds in the same namespace.
• Original authors / copyright: Jon Crall, OpenAI GPT-5.6 Thinking; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Extraction class: copied, converted to the Tau Ceti module system. Declaration names are unchanged (they already extend the canonical Mathlib namespace); references to the Courant--Fischer helpers track the redesigned API (OrthonormalBasis.spanIndices in BasisSpan.lean and the LinearMap.IsSymmetric-namespace eigenvalue results). No mathematical change.
• Spectra influence: none — this module imports only Mathlib and the sibling Basic and CourantFischer staging modules.

theorem ContinuousLinearMap.singularValues_le_norm_sub_of_rank_le {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T R : E →L[𝕜] F) (n : ℕ) (hR : (↑R).rank ≤ ↑n) : T.singularValues n ≤ ‖T - R‖

Lower Eckart--Young inequality in operator-norm form: an operator of rank at most n cannot approximate T more closely than the nth singular value of T.

theorem ContinuousLinearMap.singularValues_le_approximationNumber {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : T.singularValues n ≤ T.approximationNumber n

The nth finite-dimensional singular value is bounded by the nth approximation number. This is the lower half of the finite-dimensional Eckart--Young identification.

theorem ContinuousLinearMap.approximationNumber_eq_singularValues {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : T.approximationNumber n = T.singularValues n

Finite-dimensional Eckart--Young identification for the zero-based approximation-number convention used in this project: aₙ(T) = σₙ(T), with no index shift on either side.

Deliberately not @[simp]. It would fire on every approximationNumber goal that happens to sit under FiniteDimensional instances, rewriting the object this development is about into Mathlib's, which is the wrong normal form for a downstream perturbation argument; and unlike the other direction there is no cheap way for a consumer to opt out once it is global.

theorem ContinuousLinearMap.abs_singularValues_sub_singularValues_le {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T S : E →L[𝕜] F) (n : ℕ) : |T.singularValues n - S.singularValues n| ≤ ‖T - S‖

Weyl's inequality for singular values: |σₙ(T) − σₙ(S)| ≤ ‖T − S‖.

Every singular value is 1-Lipschitz in the operator norm — the singular-value counterpart of Weyl's eigenvalue inequality, and the standard sharp form: there is no auxiliary bound on T or S, and no factor depending on their size.

The proof is not an argument about singular values at all. It is abs_approximationNumber_sub_approximationNumber_le, which holds over any normed space with no inner product, transported through the Eckart--Young identification above. That is the payoff of stating the s-number layer field-generically: the Hilbert-space theorem is a corollary of a Banach-space one.

theorem ContinuousLinearMap.singularValues_eq_zero_iff_rank_le {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : T.singularValues n = 0 ↔ (↑T).rank ≤ ↑n

Singular values have the same exact rank cutoff as approximation numbers.