Min--max lower bounds for approximation numbers

This module proves the infinite-dimensional lower half of the Courant--Fischer characterization for approximation numbers. A uniform lower modulus on an (n+1)-dimensional test subspace forces the nth approximation number to be at least that modulus.

The other half — every strict lower bound for aₙ(T) is realized as such a modulus — is ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/MinMaxUpper.lean.

Namespace note

These declarations extend the existing Mathlib namespace ContinuousLinearMap rather than living under TauCeti, so that dot notation 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. 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/ApproximationNumberMinMax.lean at Davis--Kahan commit fc38eb48b9b49f2e1d87fe0c7022dc5e262820a7.
• Original declarations: ContinuousLinearMap.le_approximationNumber_of_finrank_lt and ContinuousLinearMap.le_approximationNumber_of_linearIndependent.
• 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). No mathematical change.
• Spectra influence: none — this module imports only Mathlib and the sibling Basic and CourantFischer staging modules.

theorem ContinuousLinearMap.le_approximationNumber_of_lt_rank {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] (T : E₁ →L[𝕜] F₁) (n : ℕ) (V : Submodule 𝕜 E₁) {c : ℝ} (hVrank : ↑n < Module.rank 𝕜 ↥V) (hV : ∀ (x : ↥V), c * ‖↑x‖ ≤ ‖T ↑x‖) : c ≤ T.approximationNumber n

Courant--Fischer lower bound for approximation numbers. If T is bounded below by c on a test subspace of rank greater than n, then the nth approximation number is at least c.

The hypothesis is stated on Module.rank, not finrank, and the bound is homogeneous rather than restricted to unit vectors. Both matter:

• rank rather than dimension means the test subspace need not be finite-dimensional, so there is no [FiniteDimensional 𝕜 V] instance to supply — an infinite-dimensional V satisfies n < Module.rank 𝕜 V for every n. The proof never uses more than "V is too big to be killed by a rank ≤ n map";
• the homogeneous bound c * ‖x‖ ≤ ‖T x‖ says something at x = 0 and scales, where a unit-vector premise does neither. le_approximationNumber_of_finrank_lt below converts from the unit-vector form, which needs no sign hypothesis on c.

Unlike the finite-dimensional Eckart--Young identification, the ambient source and target spaces need not be finite-dimensional either.

The converse is ContinuousLinearMap.exists_linearIndependent_lowerBound_of_lt_approximationNumber_complex in ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/MinMaxUpper.lean, so the characterization is complete; an earlier version of this docstring said only this half held unconditionally in infinite dimensions, which was a statement about the then-available proof, not about the mathematics.

theorem ContinuousLinearMap.le_approximationNumber_of_finrank_lt {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] (T : E₁ →L[𝕜] F₁) (n : ℕ) (V : Submodule 𝕜 E₁) [FiniteDimensional 𝕜 ↥V] {c : ℝ} (hVdim : n < Module.finrank 𝕜 ↥V) (hV : ∀ (x : ↥V), ‖↑x‖ = 1 → c ≤ ‖T ↑x‖) : c ≤ T.approximationNumber n

Finite-dimensional form of le_approximationNumber_of_lt_rank, with the unit-vector premise the classical statement uses.

Nothing is assumed about the sign of c: at x = 0 the homogeneous bound reads c * 0 ≤ 0, and elsewhere it follows by rescaling to a unit vector.

theorem ContinuousLinearMap.le_approximationNumber_of_linearIndependent {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] (T : E₁ →L[𝕜] F₁) (n : ℕ) (v : Fin (n + 1) → E₁) (hv : LinearIndependent 𝕜 v) {c : ℝ} (hV : ∀ x ∈ Submodule.span 𝕜 (Set.range v), ‖x‖ = 1 → c ≤ ‖T x‖) : c ≤ T.approximationNumber n

Family form of le_approximationNumber_of_finrank_lt: a linearly independent family of n + 1 vectors determines the required test subspace.

This is not a forgetful wrapper — it is how every downstream consumer in this repository applies the bound, since a spanning family is what the perturbation arguments produce.

The orthogonal-tail upper bound

Roadmap topic T09 §B4 asks for the intrinsic equality aₙ(T) = ⨅ {‖T ∘L (Vᗮ).starProjection‖ : finrank V ≤ n}. This is the ≤ half: every subspace of dimension at most n supplies an admissible approximation, so the approximation number is below every orthogonal tail.

theorem ContinuousLinearMap.approximationNumber_le_norm_comp_starProjection_orthogonal {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] (T : E₁ →L[𝕜] F₁) (n : ℕ) (V : Submodule 𝕜 E₁) [V.HasOrthogonalProjection] [Vᗮ.HasOrthogonalProjection] [FiniteDimensional 𝕜 ↥V] (hV : Module.finrank 𝕜 ↥V ≤ n) : T.approximationNumber n ≤ ‖T ∘SL Vᗮ.starProjection‖

Every orthogonal tail bounds the approximation number. Compressing away a subspace V of dimension at most n leaves an admissible rank-≤ n approximation, so aₙ(T) ≤ ‖T ∘L (Vᗮ).starProjection‖.

This is the easy half of the orthogonal-tail formula (T09 §B4); the reverse inequality — that the infimum over such V is attained down to aₙ(T) — is not proved here. The subspace lies in the source, and the dimension bound is finrank V ≤ n under the zero-based indexing this development uses.

The orthogonal-tail lower bound

This is the reverse inequality of T09 §B4: no admissible subspace's orthogonal tail sits below aₙ(T), so together with approximationNumber_le_norm_comp_starProjection_orthogonal the approximation number is the infimum of the tails.

The witness is the one §B4 names: given a rank-≤ n approximation R, take V := (ker R)ᗮ. Its dimension is at most the rank of R, and Vᗮ = ker R, on which R vanishes — so the tail of T over V is the tail of T - R, which is bounded by ‖T - R‖.

Completeness of the source is used exactly once, to know that the closed subspace ker R carries an orthogonal projection.

instance ContinuousLinearMap.hasOrthogonalProjection_ker {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [CompleteSpace E₁] (R : E₁ →L[𝕜] F₁) : (↑R).ker.HasOrthogonalProjection

The kernel of a bounded operator is closed, so in a complete space it carries an orthogonal projection. Registered as an instance because every statement below mentions (ker R).starProjection.

theorem ContinuousLinearMap.norm_comp_starProjection_ker_le_norm_sub {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [CompleteSpace E₁] (T R : E₁ →L[𝕜] F₁) : ‖T ∘SL (↑R).ker.starProjection‖ ≤ ‖T - R‖

An approximation is invisible on the orthogonal complement of its kernel's complement. R vanishes on ker R, so compressing T to ker R is the same as compressing T - R, and the compression cannot increase the norm.

theorem ContinuousLinearMap.rank_orthogonal_ker_le_of_rank_le {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] (R : E₁ →L[𝕜] F₁) {n : ℕ} (hR : (↑R).rank ≤ ↑n) : Module.rank 𝕜 ↥(↑R).kerᗮ ≤ ↑n

The orthogonal complement of the kernel is no bigger than the rank. R is injective on (ker R)ᗮ, which identifies that subspace with a submodule of the range.

The proof goes through Cardinal.lift rather than rank--nullity because the source and target live in independent universes, exactly as in le_approximationNumber_of_lt_rank above.

theorem ContinuousLinearMap.exists_finrank_le_norm_comp_starProjection_orthogonal_le {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [CompleteSpace E₁] (T : E₁ →L[𝕜] F₁) {n : ℕ} (R : E₁ →L[𝕜] F₁) (hR : (↑R).rank ≤ ↑n) : ∃ (V : Submodule 𝕜 E₁) (_ : FiniteDimensional 𝕜 ↥V) (x : Vᗮ.HasOrthogonalProjection), Module.finrank 𝕜 ↥V ≤ n ∧ ‖T ∘SL Vᗮ.starProjection‖ ≤ ‖T - R‖

Every rank-≤ n approximation is beaten by an admissible orthogonal tail. This is the witness half of T09 §B4's reverse inequality: the subspace V := (ker R)ᗮ lies in the source, has finrank 𝕜 V ≤ n under zero-based indexing, and its tail is no worse than R.

theorem ContinuousLinearMap.le_approximationNumber_of_forall_norm_comp_starProjection_orthogonal {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [CompleteSpace E₁] (T : E₁ →L[𝕜] F₁) (n : ℕ) {c : ℝ} (h : ∀ (V : Submodule 𝕜 E₁), FiniteDimensional 𝕜 ↥V → ∀ (x : Vᗮ.HasOrthogonalProjection), Module.finrank 𝕜 ↥V ≤ n → c ≤ ‖T ∘SL Vᗮ.starProjection‖) : c ≤ T.approximationNumber n

The orthogonal tails bound the approximation number from below. If a constant sits below every admissible tail, it sits below aₙ(T).

With approximationNumber_le_norm_comp_starProjection_orthogonal this completes T09 §B4's exact equality: aₙ(T) is the greatest lower bound of ‖T ∘L Vᗮ.starProjection‖ over subspaces V of the source with finrank 𝕜 V ≤ n.

The single-statement form is approximationNumber_eq_sInf_norm_comp_starProjection_orthogonal below, and §B4's other two conditions follow it.

theorem ContinuousLinearMap.approximationNumber_eq_sInf_norm_comp_starProjection_orthogonal {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [CompleteSpace E₁] (T : E₁ →L[𝕜] F₁) (n : ℕ) : T.approximationNumber n = sInf {r : ℝ | ∃ (V : Submodule 𝕜 E₁) (_ : FiniteDimensional 𝕜 ↥V) (x : Vᗮ.HasOrthogonalProjection), Module.finrank 𝕜 ↥V ≤ n ∧ r = ‖T ∘SL Vᗮ.starProjection‖}

The min--max formula in orthogonal-tail form (T09 §B4). The nth approximation number is the infimum of ‖T ∘L Vᗮ.starProjection‖ over finite-dimensional subspaces V of the source with finrank 𝕜 V ≤ n.

The three conditions §B4 requires of the statement are visible in it: the subspace V lies in the source, the dimension condition is finrank 𝕜 V ≤ n under zero-based indexing, and the infimum is over a nonempty bounded-below set of reals so sInf means what it says (V = ⊥ is always admissible and gives ‖T‖).

The infimum need not be attained, which is why this is a sInf and not an existence statement; the two halves it is assembled from — approximationNumber_le_norm_comp_starProjection_orthogonal and exists_finrank_le_norm_comp_starProjection_orthogonal_le — are the usable forms.

§B4's remaining two conditions are the two theorems just below: approximationNumber_eq_zero_of_finrank_source_le for the behaviour once n reaches the dimension of the source, and norm_comp_starProjection_orthogonal_eq_sSup_unitClosedBall for the equivalence with the sup formulation — on the closed unit ball of Vᗮ rather than its unit sphere, for the reason that theorem's docstring gives.

theorem ContinuousLinearMap.approximationNumber_eq_zero_of_finrank_source_le {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [FiniteDimensional 𝕜 E₁] (T : E₁ →L[𝕜] F₁) {n : ℕ} (hn : Module.finrank 𝕜 E₁ ≤ n) : T.approximationNumber n = 0

The infimum collapses once n reaches the dimension of the source (T09 §B4). V = ⊤ is then admissible, its orthogonal complement is ⊥, and the tail of T over ⊥ is the zero operator — so the infimum, and therefore aₙ(T), is 0.

This is proved from the orthogonal-tail bound rather than from the rank characterisation, which is the point: it is a statement about the infimum in §B4's sense, and reading it off the tail formula is what shows the formula behaves.

theorem ContinuousLinearMap.norm_comp_starProjection_orthogonal_eq_norm_comp_subtypeL {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] (T : E₁ →L[𝕜] F₁) (V : Submodule 𝕜 E₁) [Vᗮ.HasOrthogonalProjection] : ‖T ∘SL Vᗮ.starProjection‖ = ‖T ∘SL Vᗮ.subtypeL‖

Compressing by the projection is restricting to the subspace. The orthogonal projection maps the unit ball of E₁ onto the unit ball of Vᗮ and fixes Vᗮ, so the two operator norms coincide.

theorem ContinuousLinearMap.norm_comp_starProjection_orthogonal_eq_sSup_unitClosedBall {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] (T : E₁ →L[𝕜] F₁) (V : Submodule 𝕜 E₁) [Vᗮ.HasOrthogonalProjection] : ‖T ∘SL Vᗮ.starProjection‖ = sSup ((fun (x : ↥Vᗮ) => ‖T ↑x‖) '' Metric.closedBall 0 1)

The unit-ball formulation of the orthogonal tail (T09 §B4). The tail is the supremum of ‖T x‖ over the closed unit ball of Vᗮ, so approximationNumber_eq_sInf_norm_comp_starProjection_orthogonal is literally an inf-sup formula.

Stated on the closed ball rather than the unit sphere, deliberately: on Vᗮ = ⊥ the sphere is empty and its supremum is not the tail, whereas the ball form holds for every V.

theorem ContinuousLinearMap.approximationNumber_le_of_spectral_band {𝕜 : Type u} [RCLike 𝕜] {E₁ : Type v} {F₁ : Type w} [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup F₁] [InnerProductSpace 𝕜 F₁] [CompleteSpace E₁] {T : E₁ →L[𝕜] F₁} {P : E₁ →L[𝕜] E₁} {r : ℕ} {δ : ℝ} (hδ : 0 ≤ δ) (hidem : IsIdempotentElem P) (hsa : IsSelfAdjoint P) (hrank : (↑P).rank ≤ ↑r) (hband : ∀ (x : E₁), ‖T (x - P x)‖ ≤ δ * ‖x - P x‖) : T.approximationNumber r ≤ δ

A spectral band bounds an approximation number.

If P is an orthogonal projection of rank at most r and T is bounded by δ off its range, then aᵣ(T) ≤ δ. The competitor is T ∘L P, whose rank is at most P's.

0 ≤ δ is not defensive padding. Without it the statement is false: at P = 1 the band hypothesis reads 0 ≤ 0 and holds for any δ, and taking r ≥ finrank E makes the conclusion 0 ≤ δ, which fails at δ = -1. The submitted roadmap omitted the hypothesis; it was corrected against this counterexample, and the two signatures now agree.

hidem and hsa are used in exactly one place: they make 1 - P a star projection, hence a contraction, which is what turns the band bound δ * ‖x - P x‖ into δ * ‖x‖.