The real threshold theorem for approximation numbers

This module proves the real spectral-threshold form of the accepted complex infinite-dimensional Courant--Fischer localization theorem, together with its LUB / epsilon characterizations.

Mathlib's continuous functional calculus is available for bounded operators on complex Hilbert spaces but not directly for bounded operators on real ones, so the proof works on the complexification and descends. The transport it needs — the canonical conjugation, the descent of conjugation-fixed operators, and the complexification laws for the adjoint and the Gram operator — is ForTauCeti.Analysis.InnerProductSpace.Complexification.FunctionalCalculus. What is local to this file is the continuous high-energy spectral cutoff, which is private.

Main results

• TauCeti.ApproximationNumber.exists_linearIndependent_lowerBound_of_lt_approximationNumber_real: every strict lower bound for aₙ(T) is realized by a uniform lower modulus on a real (n+1)-dimensional subspace — the real Courant--Fischer localization;
• TauCeti.ApproximationNumber.hasMinMaxLowerBound_real: the packaged form, which is the hypothesis kyFanGauge_add_le_of_exists_finiteRestriction takes over RCLike 𝕜 and which until now only ℂ could discharge;
• TauCeti.ApproximationNumber.exists_finiteRestrictionApproximationNumber_gt_of_lt_real;
• TauCeti.ApproximationNumber.approximationNumber_isLUB_finiteRestrictions_real;
• TauCeti.ApproximationNumber.lt_approximationNumber_iff_exists_finiteDimensional_lowerBound_real.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: DavisKahan/OperatorIdeal/ApproximationNumbers/Real/Threshold.lean.
• Extraction class: moved, not restated. Of its three non-Mathlib imports, two were already ForTauCeti and the third, DavisKahan/OperatorIdeal/ApproximationNumbers/Core.lean, is an export shim whose own docstring says every declaration in it is a forwarding name — so the module depended on no mathematics in the paper library.
• Namespace TauCeti.DavisKahan.Experimental.ExactSinTheta.ApproximationNumbersReal became TauCeti.ApproximationNumber, the namespace of the approximationNumber these theorems are about. The _real suffix stays: it distinguishes each statement from its _complex twin, which is what the suffix has always meant here.
• 317 lines came off on the way in. The module carried a private copy of thirty transport lemmas that are declaration-for-declaration the public API it already imported.
• Original authors / copyright: Jon Crall, GPT-5.6 Thinking; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none.

The real algebra structure and the real continuous functional calculus on the complexified operator algebra are scoped instances of RealComplexification, opened here. They used to be reinstalled in this file as a second local instance, which made them a different declaration from the one that module's lemmas are stated against — and proving the two defeq is what timed out isDefEq when this file first tried to import them. See lane {lane:CPLX-DEDUP-3}.

Transport to the complexification

The conjugation, its induced involution on operators, and the complexification laws for the adjoint and the Gram operator all live in ForTauCeti/Analysis/InnerProductSpace/Complexification/FunctionalCalculus.lean and are opened above. This module used to carry a private copy of all thirty of them; they were identical, so the copy is gone.

The real threshold theorem

theorem TauCeti.ApproximationNumber.approximationNumber_comp_subtypeL_le_real {E : Type v} {F : Type vF} [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 real subspace cannot increase an approximation number.

The staged statement is already field-generic; this is it at ℝ.

def TauCeti.ApproximationNumber.finiteRestrictionApproximationNumbersReal {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : E →L[ℝ] F) (n : ℕ) : Set ℝ

Approximation numbers of restrictions to real spans of n+1 vectors.

Equations

• TauCeti.ApproximationNumber.finiteRestrictionApproximationNumbersReal T n = T.finiteRestrictionApproximationNumbers n

theorem TauCeti.ApproximationNumber.finiteRestrictionApproximationNumbersReal_upperBound {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : E →L[ℝ] F) (n : ℕ) : T.approximationNumber n ∈ upperBounds (finiteRestrictionApproximationNumbersReal T n)

The ambient real approximation number bounds all finite restrictions.

theorem TauCeti.ApproximationNumber.exists_linearIndependent_lowerBound_of_lt_approximationNumber_real {E : Type v} {F : Type vF} [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‖

Real spectral-threshold form of infinite-dimensional Courant--Fischer. Every strict nonnegative lower bound for a_n(T) is improved to a uniform lower modulus on a real (n+1)-dimensional subspace.

theorem TauCeti.ApproximationNumber.hasMinMaxLowerBound_real {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] : ContinuousLinearMap.HasMinMaxLowerBound ℝ E F

Over ℝ the min--max lower-bound property is the real threshold theorem above, which is where the complexification is paid for. Everything the localization theory needs from the scalar field is this one fact — see ContinuousLinearMap.HasMinMaxLowerBound.

theorem TauCeti.ApproximationNumber.exists_finiteRestrictionApproximationNumber_gt_of_lt_real {E : Type v} {F : Type vF} [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) : ∃ (v : Fin (n + 1) → E), r < (T ∘SL (Submodule.span ℝ (Set.range v)).subtypeL).approximationNumber n

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

theorem TauCeti.ApproximationNumber.approximationNumber_isLUB_finiteRestrictions_real {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (T : E →L[ℝ] F) (n : ℕ) : IsLUB (finiteRestrictionApproximationNumbersReal T n) (T.approximationNumber n)

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

theorem TauCeti.ApproximationNumber.lt_approximationNumber_iff_exists_finiteDimensional_lowerBound_real {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace 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 real generalized Courant--Fischer characterization.

theorem TauCeti.ApproximationNumber.kyFanGauge_add_le_real {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (S T : E →L[ℝ] F) (k : ℕ) : (S + T).kyFanGauge k ≤ S.kyFanGauge k + T.kyFanGauge k

The Ky Fan triangle inequality over real Hilbert spaces. The complex case is ContinuousLinearMap.kyFanGauge_add_le_complex; both are the same theorem, kyFanGauge_add_le_of_hasMinMaxLowerBound, applied to the min--max lower bound for their field. Over ℝ that bound is hasMinMaxLowerBound_real, which is where the complexification in this file is spent.

instance TauCeti.ApproximationNumber.hasMinMaxLowerBoundEverywhere_real : ContinuousLinearMap.HasMinMaxLowerBoundEverywhere ℝ

ℝ has the min--max lower bound for every pair of Hilbert spaces. With this instance every construction stated over ContinuousLinearMap.HasMinMaxLowerBoundEverywhere 𝕜 — the trace-class ideal family among them — is available at ℝ as well as at ℂ.