The min--max theorem for approximation numbers

ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/MinMax.lean proves the easy half of the Courant--Fischer characterisation: a uniform lower modulus on a test subspace of rank greater than n bounds aₙ(T) from below. This module proves the converse, which is the half that carries the content:

r < aₙ(T)  →  ∃ s > r, ∃ n + 1 independent vectors spanning a subspace on which ‖T x‖ ≥ s ‖x‖.

Together the two say that aₙ(T) is the supremum, over (n+1)-dimensional subspaces, of the lower modulus of T there — for an arbitrary bounded operator between complex Hilbert spaces, with no compactness, separability or finite-dimensionality hypothesis.

Why this is not a spectral theorem

The classical proof cuts the spectrum of |T| at s with a projection-valued measure. This one does not: ForTauCeti/Analysis/InnerProductSpace/SpectralCutoff.lean gets the same splitting of E from the continuous functional calculus, as the kernel of (|T| - s)₊ and its orthogonal complement. The proof here is then a dichotomy on that complement M:

• if M has rank greater than n, it contains n + 1 independent vectors, and |T| — hence T, by ContinuousLinearMap.norm_modulus_apply — is bounded below by s on it;
• otherwise M is finite-dimensional of dimension at most n, so T ∘L M.starProjection is an admissible rank-≤ n approximant, and it is within s of T because 1 - P_M lands in the kernel where |T| is bounded above by s. That forces aₙ(T) ≤ s, contradicting the hypothesis.

Only the second branch can fail, and it fails into a contradiction, so the first branch always holds.

Consequences

This unblocks the results that had been routed through vendor/Spectra's min--max bridge: the Ky Fan gauge triangle inequality, and with it the Ky Fan and symmetric-gauge operator ideals, and the orthogonal block-sum merge formulas.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: authored directly in ForTauCeti; it has had no prior home.
• Extraction class: authored in place for the Tau Ceti staging layer.
• Original authors / copyright: Jon Crall, Claude Opus 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none in the proof. The statement is the one DavisKahan/Interop/Spectra/ApproximationNumberMinMax.lean carried as exists_linearIndependent_lowerBound_of_lt_approximationNumber_complex, whose proof used Spectra's projection-valued measures; nothing of that proof is reused here.

theorem ContinuousLinearMap.exists_fin_linearIndependent_of_le_rank {V : Type u_1} [AddCommGroup V] [Module ℂ V] (n : ℕ) (h : ↑n ≤ Module.rank ℂ V) : ∃ (v : Fin n → V), LinearIndependent ℂ v

A module of rank at least n carries n independent vectors.

Mathlib has the one-step extension exists_linearIndependent_snoc_of_lt_rank; this is the iterate, which is what a "there are n + 1 independent vectors" statement needs.

theorem ContinuousLinearMap.exists_fin_succ_linearIndependent_of_lt_rank {V : Type u_1} [AddCommGroup V] [Module ℂ V] (n : ℕ) (h : ↑n < Module.rank ℂ V) : ∃ (v : Fin (n + 1) → V), LinearIndependent ℂ v

A module of rank greater than n carries n + 1 independent vectors.

theorem ContinuousLinearMap.exists_linearIndependent_lowerBound_of_lt_approximationNumber_complex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (T : E →L[ℂ] F) (n : ℕ) {r : ℝ} (hr0 : 0 ≤ r) (hr : r < T.approximationNumber n) : ∃ (s : ℝ), r < s ∧ ∃ (v : Fin (n + 1) → E), LinearIndependent ℂ v ∧ ∀ x ∈ Submodule.span ℂ (Set.range v), s * ‖x‖ ≤ ‖T x‖

The min--max upper bound for approximation numbers. If r is strictly below the nth approximation number of T, then T is bounded below by some s > r on a subspace spanned by n + 1 independent vectors.

This is the converse of ContinuousLinearMap.le_approximationNumber_of_linearIndependent, and the two together characterise aₙ(T) as a supremum of lower moduli. No compactness or finite-dimensionality is assumed.