Approximation-number foundation and scalar-specific analytic endpoints

This lower module contains the approximation-number definitions, scalar-generic algebraic laws, finite-dimensional Ky Fan bridge, and the accepted complex strong-cutoff and infinite-dimensional Ky Fan arguments. It intentionally does not import the real localization module, so the real proof can depend on this foundation without creating an import cycle.

The downstream ideal-family construction is ForTauCeti.Analysis.OperatorIdeal.Family; the paper library's own aggregate is DavisKahan/OperatorIdeal/ApproximationNumbers/, which is a different library and is not what a reader of this module wants.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: DavisKahan/OperatorIdeal/ApproximationNumbers/Core.lean.
• Extraction class: moved, not restated. Statements, proofs and namespace are unchanged by the move; what changed is the enclosing library, and with it the build options the file is measured against.
• Original authors / copyright: Jon Crall, OpenAI GPT-5.6 Thinking; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — imports are ForTauCeti leaves and Mathlib.

def TauCeti.ApproximationNumber.StronglyTendsto {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type w} (T : ι → E →L[𝕜] E) (l : Filter ι) (S : E →L[𝕜] E) : Prop

Strong operator convergence expressed pointwise.

Equations

• TauCeti.ApproximationNumber.StronglyTendsto T l S = ∀ (x : E), Filter.Tendsto (fun (i : ι) => (T i) x) l (nhds (S x))

def TauCeti.ApproximationNumber.IsOrthogonalProjectionMap {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (P : E →L[𝕜] E) : Prop

Orthogonal projection predicate for bounded operators.

Equations

• TauCeti.ApproximationNumber.IsOrthogonalProjectionMap P = (P ∘SL P = P ∧ (↑P).IsSymmetric)

noncomputable def TauCeti.ApproximationNumber.approximationSingularValue {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (n : ℕ) (K : E →L[𝕜] F) : ℝ

Zero-based approximation singular value, defined as the operator-norm distance to maps of rank at most n.

Equations

• TauCeti.ApproximationNumber.approximationSingularValue n K = K.approximationNumber n

theorem TauCeti.ApproximationNumber.approximationSingularValue_nonneg {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (n : ℕ) (K : E →L[𝕜] F) : 0 ≤ approximationSingularValue n K

Approximation singular values are nonnegative.

@[simp]

theorem TauCeti.ApproximationNumber.approximationSingularValue_zero_map {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (n : ℕ) : approximationSingularValue n 0 = 0

Approximation singular values of the zero map vanish.

@[simp]

theorem TauCeti.ApproximationNumber.approximationSingularValue_zero {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (K : E →L[𝕜] F) : approximationSingularValue 0 K = ‖K‖

The zero-based first approximation singular value is the operator norm.

theorem TauCeti.ApproximationNumber.approximationSingularValue_smul {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (n : ℕ) (c : 𝕜) (K : E →L[𝕜] F) : approximationSingularValue n (c • K) = ‖c‖ * approximationSingularValue n K

Approximation singular values are absolutely homogeneous.

@[simp]

theorem TauCeti.ApproximationNumber.approximationSingularValue_neg {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (n : ℕ) (K : E →L[𝕜] F) : approximationSingularValue n (-K) = approximationSingularValue n K

Approximation singular values are unchanged by negation.

theorem TauCeti.ApproximationNumber.approximationSingularValue_antitone {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (K : E →L[𝕜] F) : Antitone fun (n : ℕ) => approximationSingularValue n K

Approximation singular values decrease with the index.

theorem TauCeti.ApproximationNumber.approximationSingularValue_le_opNorm {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (n : ℕ) (K : E →L[𝕜] F) : approximationSingularValue n K ≤ ‖K‖

Every approximation singular value is controlled by operator norm.

theorem TauCeti.ApproximationNumber.approximationSingularValue_add_le {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (n : ℕ) (K L : E →L[𝕜] F) : approximationSingularValue n (K + L) ≤ approximationSingularValue n K + ‖L‖

Perturbation inequality at a fixed approximation index.

theorem TauCeti.ApproximationNumber.approximationSingularValue_adjoint {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (n : ℕ) (K : E →L[𝕜] F) : approximationSingularValue n (ContinuousLinearMap.adjoint K) = approximationSingularValue n K

Adjoint invariance of approximation singular values on Hilbert spaces.

theorem TauCeti.ApproximationNumber.approximationSingularValue_comp_le {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {G : Type vG} {H : Type vH} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (n : ℕ) (L : F →L[𝕜] G) (K : E →L[𝕜] F) (R : H →L[𝕜] E) : approximationSingularValue n (L ∘SL K ∘SL R) ≤ ‖L‖ * approximationSingularValue n K * ‖R‖

Ideal inequality for approximation singular values.

theorem TauCeti.ApproximationNumber.singularValues_le_approximationSingularValue {𝕜 : Type u} [RCLike 𝕜] {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace 𝕜 E₀] [FiniteDimensional 𝕜 E₀] [NormedAddCommGroup F₀] [InnerProductSpace 𝕜 F₀] [FiniteDimensional 𝕜 F₀] (A : E₀ →ₗ[𝕜] F₀) (n : ℕ) : A.singularValues n ≤ approximationSingularValue n (LinearMap.toContinuousLinearMap A)

On finite-dimensional Hilbert spaces, each singular value is bounded by the corresponding approximation singular value. This is the real-valued adapter for the lower Eckart--Young theorem.

theorem TauCeti.ApproximationNumber.approximationSingularValue_eq_singularValues {𝕜 : Type u} [RCLike 𝕜] {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace 𝕜 E₀] [FiniteDimensional 𝕜 E₀] [NormedAddCommGroup F₀] [InnerProductSpace 𝕜 F₀] [FiniteDimensional 𝕜 F₀] (A : E₀ →ₗ[𝕜] F₀) (n : ℕ) : approximationSingularValue n (LinearMap.toContinuousLinearMap A) = A.singularValues n

On finite-dimensional Hilbert spaces, approximation singular values are exactly the ordinary singular values.

theorem TauCeti.ApproximationNumber.IsOrthogonalProjectionMap.norm_apply_le {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {P : E →L[𝕜] E} (hP : IsOrthogonalProjectionMap P) (x : E) : ‖P x‖ ≤ ‖x‖

An orthogonal projection does not increase vector norms.

theorem TauCeti.ApproximationNumber.IsOrthogonalProjectionMap.norm_le_one {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {P : E →L[𝕜] E} (hP : IsOrthogonalProjectionMap P) : ‖P‖ ≤ 1

An orthogonal projection has operator norm at most one.

theorem TauCeti.ApproximationNumber.tendsto_opNorm_zero_of_finiteDimensional {𝕜 : Type u} [RCLike 𝕜] {ι : Type w} {l : Filter ι} {V : Type vG} {G : Type vH} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (T : ι → V →L[𝕜] G) (hT : ∀ (x : V), Filter.Tendsto (fun (i : ι) => (T i) x) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => ‖T i‖) l (nhds 0)

On a finite-dimensional source, pointwise convergence of bounded linear maps to zero upgrades to convergence in operator norm.

theorem TauCeti.ApproximationNumber.approximationSingularValue_comp_le_of_isOrthogonalProjection {𝕜 : Type u} [RCLike 𝕜] {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace 𝕜 E₀] [NormedAddCommGroup F₀] [InnerProductSpace 𝕜 F₀] {P : E₀ →L[𝕜] E₀} (hP : IsOrthogonalProjectionMap P) (n : ℕ) (K : E₀ →L[𝕜] F₀) : approximationSingularValue n (K ∘SL P) ≤ approximationSingularValue n K

Post-composing with an orthogonal projection cannot raise an approximation number. A projection is a contraction, so this is the ideal inequality with ‖P‖ ≤ 1 discharged.

Extracted from the convergence theorem below, where it was the hUpper half: it is a statement about one projection with no net in sight, and it is the half a reader can check without reading the localization argument.

theorem TauCeti.ApproximationNumber.approximationSingularValue_comp_strongProjection_tendsto_of_minMax {𝕜 : Type u} [RCLike 𝕜] {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace 𝕜 E₀] [NormedAddCommGroup F₀] [InnerProductSpace 𝕜 F₀] (hlb : ContinuousLinearMap.HasMinMaxLowerBound 𝕜 E₀ F₀) {ι : Type w} {P : ι → E₀ →L[𝕜] E₀} {l : Filter ι} (hPproj : ∀ (i : ι), IsOrthogonalProjectionMap (P i)) (hP : StronglyTendsto P l (ContinuousLinearMap.id 𝕜 E₀)) (n : ℕ) (K : E₀ →L[𝕜] F₀) : Filter.Tendsto (fun (i : ι) => approximationSingularValue n (K ∘SL P i)) l (nhds (approximationSingularValue n K))

Cutoff convergence. Along a net of orthogonal projections converging strongly to the identity, every approximation number of K ∘L P i converges to the corresponding approximation number of K.

Upper semicontinuity is free (P i is a contraction); the lower bound is where the generalized Courant--Fischer localization enters, and it is the only step that depends on the scalar field, so it is taken as the hypothesis ContinuousLinearMap.HasMinMaxLowerBound.

theorem TauCeti.ApproximationNumber.approximationSingularValue_comp_strongProjection_tendsto_complex {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace ℂ E₀] [CompleteSpace E₀] [NormedAddCommGroup F₀] [InnerProductSpace ℂ F₀] [CompleteSpace F₀] {ι : Type w} {P : ι → E₀ →L[ℂ] E₀} {l : Filter ι} (hPproj : ∀ (i : ι), IsOrthogonalProjectionMap (P i)) (hP : StronglyTendsto P l (ContinuousLinearMap.id ℂ E₀)) (n : ℕ) (K : E₀ →L[ℂ] F₀) : Filter.Tendsto (fun (i : ι) => approximationSingularValue n (K ∘SL P i)) l (nhds (approximationSingularValue n K))

Cutoff convergence over ℂ.

noncomputable def TauCeti.ApproximationNumber.kyFanApproximationGauge {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (k : ℕ) (K : E →L[𝕜] F) : ℝ

Finite Ky Fan gauge built from approximation singular values.

This is ContinuousLinearMap.kyFanGauge with the arguments in the paper's order; the theory lives in ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/KyFan.lean and every statement below delegates to it.

Equations

• TauCeti.ApproximationNumber.kyFanApproximationGauge k K = K.kyFanGauge k

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_eq_kyFanGauge {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (k : ℕ) (K : E →L[𝕜] F) : kyFanApproximationGauge k K = K.kyFanGauge k

The approximation-number Ky Fan gauge agrees definitionally with the Ky Fan gauge.

@[simp]

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_neg {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (k : ℕ) (K : E →L[𝕜] F) : kyFanApproximationGauge k (-K) = kyFanApproximationGauge k K

Finite Ky Fan gauges are unchanged by negation.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_comp_strongProjection_tendsto_of_minMax {𝕜 : Type u} [RCLike 𝕜] {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace 𝕜 E₀] [NormedAddCommGroup F₀] [InnerProductSpace 𝕜 F₀] (hlb : ContinuousLinearMap.HasMinMaxLowerBound 𝕜 E₀ F₀) {ι : Type w} {P : ι → E₀ →L[𝕜] E₀} {l : Filter ι} (hPproj : ∀ (i : ι), IsOrthogonalProjectionMap (P i)) (hP : StronglyTendsto P l (ContinuousLinearMap.id 𝕜 E₀)) (k : ℕ) (K : E₀ →L[𝕜] F₀) : Filter.Tendsto (fun (i : ι) => kyFanApproximationGauge k (K ∘SL P i)) l (nhds (kyFanApproximationGauge k K))

Finite Ky Fan approximation gauges converge under strong orthogonal cutoffs: the termwise statement summed over Finset.range k.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_comp_strongProjection_tendsto_complex {E₁ : Type vE0} {F₁ : Type vF0} [NormedAddCommGroup E₁] [InnerProductSpace ℂ E₁] [CompleteSpace E₁] [NormedAddCommGroup F₁] [InnerProductSpace ℂ F₁] [CompleteSpace F₁] {ι : Type w} {P : ι → E₁ →L[ℂ] E₁} {l : Filter ι} (hPproj : ∀ (i : ι), IsOrthogonalProjectionMap (P i)) (hP : StronglyTendsto P l (ContinuousLinearMap.id ℂ E₁)) (k : ℕ) (K : E₁ →L[ℂ] F₁) : Filter.Tendsto (fun (i : ι) => kyFanApproximationGauge k (K ∘SL P i)) l (nhds (kyFanApproximationGauge k K))

Finite Ky Fan approximation gauges converge under complex strong orthogonal cutoffs.

theorem TauCeti.ApproximationNumber.kyFanSum_le_kyFanApproximationGauge {𝕜 : Type u} [RCLike 𝕜] {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace 𝕜 E₀] [FiniteDimensional 𝕜 E₀] [NormedAddCommGroup F₀] [InnerProductSpace 𝕜 F₀] [FiniteDimensional 𝕜 F₀] (k : ℕ) (A : E₀ →ₗ[𝕜] F₀) : kyFanSum k A ≤ kyFanApproximationGauge k (LinearMap.toContinuousLinearMap A)

The rectangular Ky Fan sum is bounded by the approximation-number gauge.

theorem TauCeti.ApproximationNumber.kyFanSum_eq_kyFanApproximationGauge {𝕜 : Type u} [RCLike 𝕜] {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace 𝕜 E₀] [FiniteDimensional 𝕜 E₀] [NormedAddCommGroup F₀] [InnerProductSpace 𝕜 F₀] [FiniteDimensional 𝕜 F₀] (k : ℕ) (A : E₀ →ₗ[𝕜] F₀) : kyFanSum k A = kyFanApproximationGauge k (LinearMap.toContinuousLinearMap A)

In finite dimensions the two agree: the rectangular Ky Fan sum is the approximation-number gauge.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_add_le_finiteDimensional {𝕜 : Type u} [RCLike 𝕜] {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace 𝕜 E₀] [FiniteDimensional 𝕜 E₀] [NormedAddCommGroup F₀] [InnerProductSpace 𝕜 F₀] [FiniteDimensional 𝕜 F₀] (k : ℕ) (A B : E₀ →ₗ[𝕜] F₀) : kyFanApproximationGauge k (LinearMap.toContinuousLinearMap (A + B)) ≤ kyFanApproximationGauge k (LinearMap.toContinuousLinearMap A) + kyFanApproximationGauge k (LinearMap.toContinuousLinearMap B)

Subadditivity of the Ky Fan gauge in finite dimensions.

theorem TauCeti.ApproximationNumber.approximationSingularValue_restrict_mono {𝕜 : Type u} [RCLike 𝕜] {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace 𝕜 E₀] [NormedAddCommGroup F₀] [InnerProductSpace 𝕜 F₀] (T : E₀ →L[𝕜] F₀) (n : ℕ) {U V : Submodule 𝕜 E₀} (hUV : U ≤ V) : approximationSingularValue n (T ∘SL U.subtypeL) ≤ approximationSingularValue n (T ∘SL V.subtypeL)

Approximation singular values are monotone in the restricted subspace: enlarging the domain cannot decrease them.

theorem TauCeti.ApproximationNumber.approximationSingularValue_orthogonalProjectionOnto_comp_eq {𝕜 : Type u} [RCLike 𝕜] {V : Type vG} {G : Type vH} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (W : Submodule 𝕜 G) [W.HasOrthogonalProjection] (A : V →L[𝕜] G) (hA : ∀ (x : V), A x ∈ W) (n : ℕ) : approximationSingularValue n (W.orthogonalProjectionOnto ∘SL A) = approximationSingularValue n A

Composing with the orthogonal projection onto the range leaves every approximation singular value unchanged.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_orthogonalProjectionOnto_comp_eq {𝕜 : Type u} [RCLike 𝕜] {V : Type vG} {G : Type vH} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (W : Submodule 𝕜 G) [W.HasOrthogonalProjection] (A : V →L[𝕜] G) (hA : ∀ (x : V), A x ∈ W) (k : ℕ) : kyFanApproximationGauge k (W.orthogonalProjectionOnto ∘SL A) = kyFanApproximationGauge k A

Composing with the orthogonal projection onto the range leaves the Ky Fan gauge unchanged.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_add_le_finiteSource {𝕜 : Type u} [RCLike 𝕜] {V : Type vG} {G : Type vH} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (k : ℕ) (A B : V →L[𝕜] G) : kyFanApproximationGauge k (A + B) ≤ kyFanApproximationGauge k A + kyFanApproximationGauge k B

Subadditivity of the Ky Fan gauge for finite-source operators.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_add_le_of_minMax {𝕜 : Type u} [RCLike 𝕜] {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace 𝕜 E₀] [NormedAddCommGroup F₀] [InnerProductSpace 𝕜 F₀] (hlb : ContinuousLinearMap.HasMinMaxLowerBound 𝕜 E₀ F₀) (k : ℕ) (K L : E₀ →L[𝕜] F₀) : kyFanApproximationGauge k (K + L) ≤ kyFanApproximationGauge k K + kyFanApproximationGauge k L

The Ky Fan triangle inequality, at whichever field supplies the min--max lower bound. The localization argument is kyFanGauge_add_le_of_exists_finiteRestriction; the field enters only through hlb.

theorem TauCeti.ApproximationNumber.exists_finiteRestrictionApproximationNumber_add_gt {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace ℂ E₀] [CompleteSpace E₀] [NormedAddCommGroup F₀] [InnerProductSpace ℂ F₀] [CompleteSpace 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 + ε

Approximation numbers are approached from below by finite restrictions: for every ε > 0 some finitely-spanned restriction comes within ε.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_add_le_complex {E₀ : Type vE0} {F₀ : Type vF0} [NormedAddCommGroup E₀] [InnerProductSpace ℂ E₀] [CompleteSpace E₀] [NormedAddCommGroup F₀] [InnerProductSpace ℂ F₀] [CompleteSpace F₀] (k : ℕ) (K L : E₀ →L[ℂ] F₀) : kyFanApproximationGauge k (K + L) ≤ kyFanApproximationGauge k K + kyFanApproximationGauge k L

Subadditivity of the Ky Fan gauge over ℂ.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_zero {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : kyFanApproximationGauge 0 0 = 0

The zero-term Ky Fan gauge vanishes.

@[simp]

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_zero_map {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (k : ℕ) : kyFanApproximationGauge k 0 = 0

Every finite Ky Fan gauge vanishes on the zero operator.

@[simp]

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_one {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (K : E →L[𝕜] F) : kyFanApproximationGauge 1 K = ‖K‖

The first positive Ky Fan gauge is operator norm.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_smul {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (k : ℕ) (c : 𝕜) (K : E →L[𝕜] F) : kyFanApproximationGauge k (c • K) = ‖c‖ * kyFanApproximationGauge k K

Ky Fan approximation gauges are absolutely homogeneous.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_nonneg {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (k : ℕ) (K : E →L[𝕜] F) : 0 ≤ kyFanApproximationGauge k K

Ky Fan approximation gauges are nonnegative.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_adjoint {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (k : ℕ) (K : E →L[𝕜] F) : kyFanApproximationGauge k (ContinuousLinearMap.adjoint K) = kyFanApproximationGauge k K

Ky Fan approximation gauges are invariant under adjoint.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_comp_le {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {G H : Type v} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (k : ℕ) (L : F →L[𝕜] G) (K : E →L[𝕜] F) (R : H →L[𝕜] E) : kyFanApproximationGauge k (L ∘SL K ∘SL R) ≤ ‖L‖ * kyFanApproximationGauge k K * ‖R‖

Two-sided ideal inequality for finite Ky Fan gauges.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_comp_eq_of_leftInverse {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {G : Type vG} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] {ι : F →L[𝕜] G} {π : G →L[𝕜] F} (hπι : Function.LeftInverse ⇑π ⇑ι) (hι : ‖ι‖ ≤ 1) (hπ : ‖π‖ ≤ 1) (k : ℕ) (K : E →L[𝕜] F) : kyFanApproximationGauge k (ι ∘SL K) = kyFanApproximationGauge k K

Enlarging the codomain leaves the finite Ky Fan gauge unchanged, for a contraction ι : F →L[𝕜] G admitting a contractive left inverse π. This is what lets an argument that needs k orthonormal vectors in the codomain run even when F has too few: pad F to G, run the argument there, and read the answer back. See ContinuousLinearMap.kyFanGauge_comp_eq_of_leftInverse.

theorem TauCeti.ApproximationNumber.opNorm_le_kyFanApproximationGauge {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {k : ℕ} (hk : 0 < k) (K : E →L[𝕜] F) : ‖K‖ ≤ kyFanApproximationGauge k K

The operator norm is the first term of every positive finite Ky Fan gauge.

theorem TauCeti.ApproximationNumber.kyFanApproximationGauge_le_nat_mul_opNorm {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (k : ℕ) (K : E →L[𝕜] F) : kyFanApproximationGauge k K ≤ ↑k * ‖K‖

A finite Ky Fan gauge is bounded by k times operator norm.

theorem TauCeti.ApproximationNumber.exists_orthonormal_kyFanApproximationGauge_sub_le_re_sum_inner {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (hlb : ContinuousLinearMap.HasMinMaxLowerBound 𝕜 E F) (K : E →L[𝕜] F) {k : ℕ} {ε : ℝ} (hε : 0 < ε) {x : Fin k → E} (hx : Orthonormal 𝕜 x) {y : Fin k → F} (hy : Orthonormal 𝕜 y) : ∃ (u : Fin k → F) (v : Fin k → E), Orthonormal 𝕜 u ∧ Orthonormal 𝕜 v ∧ kyFanApproximationGauge k K - ε ≤ RCLike.re (∑ i : Fin k, inner 𝕜 (u i) (K (v i)))

The Ky Fan gauge is approached by orthonormal pairings.

For a bounded K : E →L[𝕜] F and any ε > 0 there are orthonormal k-families v in E and u in F with kyFanApproximationGauge k K - ε ≤ re ∑ᵢ ⟪uᵢ, K vᵢ⟫. Together with the reverse inequality this says the gauge is the supremum of those pairings.

Only the approximate form is available at this generality, and that is not a defect of the proof: for a noncompact K the supremum need not be attained. With K diagonal with entries 1 - 1/n on an orthonormal basis every approximation number equals 1, so the gauge is k, while ‖K x‖ < ‖x‖ for every x ≠ 0 makes each pairing strictly smaller.

The two orthonormal families x and y are hypotheses, not conclusions: they say only that E and F have room for k orthonormal vectors, without which no such u, v can exist.

The min--max lower bound hlb is what turns the ambient approximation numbers into approximation numbers of a finite-dimensional restriction; the finite-dimensional rectangular Ky Fan principle exists_orthonormal_re_sum_inner_map_eq_kyFanSum then attains them exactly, and the compression is transported back along the inclusion and the projection, which are isometric on the vectors involved.

theorem TauCeti.ApproximationNumber.exists_orthonormal_kyFanApproximationGauge_sub_le_re_sum_inner_complex {E₂ : Type vE0} {F₂ : Type vF0} [NormedAddCommGroup E₂] [InnerProductSpace ℂ E₂] [CompleteSpace E₂] [NormedAddCommGroup F₂] [InnerProductSpace ℂ F₂] [CompleteSpace F₂] (K : E₂ →L[ℂ] F₂) {k : ℕ} {ε : ℝ} (hε : 0 < ε) {x : Fin k → E₂} (hx : Orthonormal ℂ x) {y : Fin k → F₂} (hy : Orthonormal ℂ y) : ∃ (u : Fin k → F₂) (v : Fin k → E₂), Orthonormal ℂ u ∧ Orthonormal ℂ v ∧ kyFanApproximationGauge k K - ε ≤ RCLike.re (∑ i : Fin k, inner ℂ (u i) (K (v i)))

The Ky Fan gauge is approached by orthonormal pairings, over ℂ.

The min--max lower bound is discharged by hasMinMaxLowerBound_complex, so no hypothesis on the scalar field remains.