Finite-dimensional localization of approximation numbers #

The nth approximation number of a bounded operator between Hilbert spaces is already determined by the restrictions of the operator to (n+1)-generated subspaces of its source:

aₙ(T) = sSup { aₙ (T ∘L (span {v 0, …, v n}).subtypeL) | v : Fin (n + 1) → E }.

The supremum is a genuine least upper bound (approximationNumber_isLUB_finiteRestrictions), not merely a bound, and the family is indexed by all families of n + 1 vectors — linearly dependent ones are harmless, contributing restrictions to smaller subspaces.

Main results #

ContinuousLinearMap.approximationNumber_comp_subtypeL_le: restricting the source cannot increase an approximation number. Stated for a general RCLike field;
ContinuousLinearMap.exists_finiteRestrictionApproximationNumber_gt_of_lt: every strict lower bound is exceeded by one of the restrictions;
ContinuousLinearMap.approximationNumber_isLUB_finiteRestrictions: the two together;
ContinuousLinearMap.lt_approximationNumber_iff_exists_finiteDimensional_lowerBound: the epsilon form of the min--max characterisation, packaging ContinuousLinearMap.exists_linearIndependent_lowerBound_of_lt_approximationNumber_complex with its converse ContinuousLinearMap.le_approximationNumber_of_linearIndependent into an Iff.

Provenance #

Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
Original module: DavisKahan/Interop/Spectra/ApproximationNumberMinMax.lean.
Original declarations: TauCeti.DavisKahan.Experimental.{ approximationNumber_comp_subtypeL_le, finiteRestrictionApproximationNumbers, finiteRestrictionApproximationNumbers_upperBound, exists_finiteRestrictionApproximationNumber_gt_of_lt, approximationNumber_isLUB_finiteRestrictions, lt_approximationNumber_iff_exists_finiteDimensional_lowerBound}.
Original authors / copyright: Jon Crall, OpenAI GPT-5.6 Thinking; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
Extraction class: copied and renamespaced. The statements are unchanged apart from the generalisation of approximationNumber_comp_subtypeL_le to an arbitrary RCLike field; the declarations move from TauCeti.DavisKahan.Experimental to ContinuousLinearMap, so that dot notation resolves.
Spectra influence: none. The module was under DavisKahan/Interop/Spectra/ because its threshold theorem was once proved from vendor/Spectra's projection-valued measures. That proof was replaced on 2026-07-28 by ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/MinMaxUpper.lean, after which nothing here touched Spectra and the module belonged in the staging layer.

source

theorem ContinuousLinearMap.approximationNumber_comp_subtypeL_le {𝕜 : 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) :

(T ∘SL V.subtypeL).approximationNumber n ≤ T.approximationNumber n

Restriction to a subspace cannot increase an approximation number.

source

def ContinuousLinearMap.finiteRestrictionApproximationNumbers {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) :

Set ℝ

The approximation numbers of the restrictions of T to the spans of n + 1 vectors.

Linearly dependent families are deliberately not excluded: they merely contribute restrictions to subspaces of smaller dimension, which the supremum ignores.

Equations

T.finiteRestrictionApproximationNumbers n = Set.range fun (v : Fin (n + 1) → E) => (T ∘SL (Submodule.span 𝕜 (Set.range v)).subtypeL).approximationNumber n

Instances For

source

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

T.approximationNumber n ∈ upperBounds (T.finiteRestrictionApproximationNumbers n)

The ambient approximation number bounds every finite restriction.

source

def ContinuousLinearMap.HasMinMaxLowerBound (𝕜 : Type u) [RCLike 𝕜] (E : Type v) (F : Type w) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] :

Prop

The min--max lower-bound property for a pair of Hilbert spaces over 𝕜: strictly below every approximation number of every T : E →L[𝕜] F there is a strictly larger uniform lower modulus, attained on the span of n + 1 independent vectors.

This is the only input to the approximation-number localization theory that depends on the scalar field. Over ℂ it is the min--max theorem ContinuousLinearMap.exists_linearIndependent_lowerBound_of_lt_approximationNumber_complex, proved from the continuous functional calculus on T.modulus; over ℝ, where that calculus is not available for operators on the space itself, it is transported through the complexification. Everything downstream — the finite-restriction localization, the least-upper-bound characterisation, and through them the Ky Fan triangle inequality — is stated once against this predicate rather than twice, once per field.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem ContinuousLinearMap.HasMinMaxLowerBound.exists_finiteRestrictionApproximationNumber_gt_of_lt {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (h : HasMinMaxLowerBound 𝕜 E F) (T : E →L[𝕜] F) (n : ℕ) {r : ℝ} (hr0 : 0 ≤ r) (hr : r < T.approximationNumber n) :

∃ (v : Fin (n + 1) → E), r < (T ∘SL (Submodule.span 𝕜 (Set.range v)).subtypeL).approximationNumber n

Every strict lower threshold for the ambient approximation number is exceeded by an approximation number of an (n+1)-generated restriction.

source

theorem ContinuousLinearMap.HasMinMaxLowerBound.approximationNumber_isLUB_finiteRestrictions {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (h : HasMinMaxLowerBound 𝕜 E F) (T : E →L[𝕜] F) (n : ℕ) :

IsLUB (T.finiteRestrictionApproximationNumbers n) (T.approximationNumber n)

Exact finite-dimensional localization. The ambient approximation number is the least upper bound of the approximation numbers of the restrictions to spans of n + 1 vectors.

Approximation numbers are real-valued, so IsLUB is the conditionally-complete formulation appropriate to ℝ; the family is nonempty and bounded above by the ambient approximation number.

source

theorem ContinuousLinearMap.HasMinMaxLowerBound.lt_approximationNumber_iff_exists_finiteDimensional_lowerBound {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (h : HasMinMaxLowerBound 𝕜 E F) (T : E →L[𝕜] F) (n : ℕ) {r : ℝ} (hr0 : 0 ≤ r) :

r < T.approximationNumber n ↔ ∃ (s : ℝ), r < s ∧ ∃ (v : Fin (n + 1) → E), LinearIndependent 𝕜 v ∧ ∀ x ∈ Submodule.span 𝕜 (Set.range v), s * ‖x‖ ≤ ‖T x‖

Epsilon form of the min--max characterisation. r is strictly below aₙ(T) exactly when T has a strictly larger uniform lower modulus on some (n+1)-dimensional subspace.

The forward direction is the hypothesis and the reverse is ContinuousLinearMap.le_approximationNumber_of_linearIndependent, so this is the statement in which both halves of the min--max theorem appear together.

source

theorem ContinuousLinearMap.HasMinMaxLowerBound.exists_finiteRestrictionApproximationNumber_add_gt {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (h : HasMinMaxLowerBound 𝕜 E F) (T : E →L[𝕜] F) (n : ℕ) (ε : ℝ) (hε : 0 < ε) :

∃ (v : Fin (n + 1) → E), T.approximationNumber n < (T ∘SL (Submodule.span 𝕜 (Set.range v)).subtypeL).approximationNumber n + ε

Every positive tolerance admits a finite source restriction whose approximation number is within that tolerance of the ambient one. This is the exact hypothesis ContinuousLinearMap.kyFanGauge_add_le_of_exists_finiteRestriction consumes, so it is the last step before the Ky Fan triangle inequality holds over any field with a min--max lower bound rather than over ℂ alone.

source

class ContinuousLinearMap.HasMinMaxLowerBoundEverywhere (𝕜 : Type u) [RCLike 𝕜] :

Prop

The min--max lower bound, as a property of the scalar field alone.

HasMinMaxLowerBound is a statement about one pair of spaces. An operator ideal family, by contrast, has to supply its laws for every pair at once, so it cannot take that predicate as an argument — it needs the field to satisfy it uniformly. This class is that quantification and nothing more.

Both fields are instances: hasMinMaxLowerBoundEverywhere_complex from the functional calculus, TauCeti.ApproximationNumber.hasMinMaxLowerBoundEverywhere_real by complexification. Together they are what lets the trace-class family be built once over RCLike 𝕜 rather than once per field.

Note what it does not assume: the Ky Fan triangle inequality itself. Assuming that would be assuming a theorem, and this class is one layer below it — the inequality is derived, in ContinuousLinearMap.kyFanGauge_add_le_of_hasMinMaxLowerBound.