Ky Fan gauges of approximation numbers

The kth Ky Fan gauge of a bounded operator is the sum of its first k approximation numbers,

T.kyFanGauge k = ∑ n ∈ Finset.range k, T.approximationNumber n,

so kyFanGauge 1 is the operator norm and the gauges increase to the nuclear norm. Each is a norm on the two-sided ideal it defines, and the family of them determines every unitarily invariant norm — which is why the Ky Fan gauges, not the individual approximation numbers, are what an operator-ideal theory is built from.

The triangle inequality

Everything else here is a one-line consequence of the corresponding statement about approximation numbers. The exception, and the reason this module exists, is

(S + T).kyFanGauge k ≤ S.kyFanGauge k + T.kyFanGauge k,

which is false term by term — aₙ is not subadditive — and is proved in three steps:

1. in finite dimensions it is the Ky Fan norm inequality of ForTauCeti/Analysis/InnerProductSpace/KyFan, transported along ContinuousLinearMap.approximationNumber_eq_singularValues;
2. for a finite-dimensional source and arbitrary codomain, compress the codomain to the (finite-dimensional) range of S ⊕ T, which changes no approximation number;
3. in general, localize: aₙ(S + T) is approached by the restrictions of S + T to (n+1)-generated subspaces (ContinuousLinearMap.exists_finiteRestrictionApproximationNumber_gt_of_lt), and k of those subspaces can be spanned together into a single finite-dimensional V on which step 2 applies.

Step 3 is where this used to depend on vendor/Spectra: the localization statement was proved there from projection-valued measures. It is now ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/MinMaxUpper.lean, so the whole chain is Mathlib-only. Steps 2 and 3 are stated over ℂ because that is where the min--max theorem lives.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: DavisKahan/OperatorIdeal/ApproximationNumbers/Core.lean.
• Original declarations: TauCeti.DavisKahan.Experimental.ExactSinTheta.{ kyFanApproximationGauge, kyFanApproximationGauge_neg, kyFanApproximationGauge_zero, kyFanApproximationGauge_zero_map, kyFanApproximationGauge_one, kyFanApproximationGauge_smul, kyFanApproximationGauge_nonneg, kyFanApproximationGauge_adjoint, kyFanApproximationGauge_comp_le, opNorm_le_kyFanApproximationGauge, kyFanApproximationGauge_le_nat_mul_opNorm, kyFanSum_le_kyFanApproximationGauge, kyFanSum_eq_kyFanApproximationGauge, kyFanApproximationGauge_add_le_finiteDimensional, approximationSingularValue_restrict_mono, approximationSingularValue_orthogonalProjectionOnto_comp_eq, kyFanApproximationGauge_orthogonalProjectionOnto_comp_eq, kyFanApproximationGauge_add_le_finiteSource, exists_finiteRestrictionApproximationNumber_add_gt, kyFanApproximationGauge_add_le_complex}.
• Original authors / copyright: Jon Crall, OpenAI GPT-5.6 Thinking; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Extraction class: copied and renamespaced. The gauge moves to ContinuousLinearMap.kyFanGauge with the operator first so dot notation resolves, and approximationSingularValue n K is spelled K.approximationNumber n throughout — it was only ever an alias for it. No proof was changed except for those renamings.
• Spectra influence: none, as of the replacement of the min--max bridge on 2026-07-28.

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

The kth Ky Fan gauge: the sum of the first k approximation numbers.

Equations

• T.kyFanGauge k = ∑ n ∈ Finset.range k, T.approximationNumber n

@[simp]

theorem ContinuousLinearMap.approximationNumber_neg {𝕜 : 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 = T.approximationNumber n

Approximation numbers are unchanged by negation. Mathlib's staging layer has approximationNumber_smul but not this special case.

@[simp]

theorem ContinuousLinearMap.kyFanGauge_neg {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (k : ℕ) : (-T).kyFanGauge k = T.kyFanGauge k

Ky Fan gauges are unchanged by negation.

@[simp]

theorem ContinuousLinearMap.kyFanGauge_zero_index {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) : T.kyFanGauge 0 = 0

The zeroth Ky Fan gauge is the empty sum, hence zero.

@[simp]

theorem ContinuousLinearMap.kyFanGauge_zero {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (k : ℕ) : kyFanGauge 0 k = 0

The zero operator has zero Ky Fan gauge at every index.

@[simp]

theorem ContinuousLinearMap.kyFanGauge_one {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) : T.kyFanGauge 1 = ‖T‖

The first Ky Fan gauge is the operator norm.

theorem ContinuousLinearMap.kyFanGauge_smul {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (c : 𝕜) (T : E →L[𝕜] F) (k : ℕ) : (c • T).kyFanGauge k = ‖c‖ * T.kyFanGauge k

Ky Fan gauges are absolutely homogeneous.

theorem ContinuousLinearMap.kyFanGauge_nonneg {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (k : ℕ) : 0 ≤ T.kyFanGauge k

Ky Fan gauges are nonnegative.

theorem ContinuousLinearMap.kyFanGauge_comp_le {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {G : Type x} {H : Type y} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (L : F →L[𝕜] G) (T : E →L[𝕜] F) (R : H →L[𝕜] E) (k : ℕ) : (L ∘SL T ∘SL R).kyFanGauge k ≤ ‖L‖ * T.kyFanGauge k * ‖R‖

The two-sided ideal inequality.

theorem ContinuousLinearMap.kyFanGauge_comp_eq_of_leftInverse {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {G : Type x} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] {ι : F →L[𝕜] G} {π : G →L[𝕜] F} (hπι : Function.LeftInverse ⇑π ⇑ι) (hι : ‖ι‖ ≤ 1) (hπ : ‖π‖ ≤ 1) (T : E →L[𝕜] F) (k : ℕ) : (ι ∘SL T).kyFanGauge k = T.kyFanGauge k

Ky Fan gauges do not see an enlargement of the codomain, since the approximation numbers do not: ι is a contraction of F into G and π a contractive left inverse, the model being the inclusion of F as one summand of an ℓ² direct sum together with the projection back onto it. See ContinuousLinearMap.approximationNumber_comp_eq_of_leftInverse.

theorem ContinuousLinearMap.opNorm_le_kyFanGauge {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) {k : ℕ} (hk : 0 < k) : ‖T‖ ≤ T.kyFanGauge k

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

theorem ContinuousLinearMap.kyFanGauge_le_nat_mul_opNorm {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (k : ℕ) : T.kyFanGauge k ≤ ↑k * ‖T‖

Every Ky Fan gauge is bounded by k times the operator norm, so the ideal it defines contains every bounded operator when k is finite.

theorem ContinuousLinearMap.kyFanGauge_adjoint {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (k : ℕ) : (adjoint T).kyFanGauge k = T.kyFanGauge k

Ky Fan gauges are adjoint-invariant, since the approximation numbers are.

theorem ContinuousLinearMap.kyFanSum_eq_kyFanGauge {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (k : ℕ) (A : E →ₗ[𝕜] F) : TauCeti.kyFanSum k A = (LinearMap.toContinuousLinearMap A).kyFanGauge k

In finite dimensions the Ky Fan gauge is the rectangular Ky Fan singular-value sum.

theorem ContinuousLinearMap.kyFanGauge_add_le_of_finiteDimensional {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (k : ℕ) (A B : E →ₗ[𝕜] F) : (LinearMap.toContinuousLinearMap (A + B)).kyFanGauge k ≤ (LinearMap.toContinuousLinearMap A).kyFanGauge k + (LinearMap.toContinuousLinearMap B).kyFanGauge k

Step 1 of the triangle inequality: the finite-dimensional case, transported from the rectangular Ky Fan norm.

theorem ContinuousLinearMap.approximationNumber_restrict_mono {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) {U V : Submodule 𝕜 E} (hUV : U ≤ V) : (T ∘SL U.subtypeL).approximationNumber n ≤ (T ∘SL V.subtypeL).approximationNumber n

Restricting to a larger source subspace can only increase an approximation number.

theorem ContinuousLinearMap.approximationNumber_orthogonalProjectionOnto_comp_eq {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (W : Submodule 𝕜 F) [W.HasOrthogonalProjection] (A : E →L[𝕜] F) (hA : ∀ (x : E), A x ∈ W) (n : ℕ) : (W.orthogonalProjectionOnto ∘SL A).approximationNumber n = A.approximationNumber n

Compressing the codomain to a subspace that already contains the range preserves every approximation number.

theorem ContinuousLinearMap.kyFanGauge_orthogonalProjectionOnto_comp_eq {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (W : Submodule 𝕜 F) [W.HasOrthogonalProjection] (A : E →L[𝕜] F) (hA : ∀ (x : E), A x ∈ W) (k : ℕ) : (W.orthogonalProjectionOnto ∘SL A).kyFanGauge k = A.kyFanGauge k

The Ky Fan form of approximationNumber_orthogonalProjectionOnto_comp_eq.

theorem ContinuousLinearMap.kyFanGauge_add_le_of_finiteDimensional_source {𝕜 : Type u} [RCLike 𝕜] {V : Type v} {G : Type w} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (k : ℕ) (A B : V →L[𝕜] G) : (A + B).kyFanGauge k ≤ A.kyFanGauge k + B.kyFanGauge k

Step 2 of the triangle inequality: a finite-dimensional source and an arbitrary Hilbert codomain. The codomain is compressed onto the range of A ⊕ B, which is finite-dimensional and changes no approximation number.

theorem ContinuousLinearMap.kyFanGauge_add_le_of_exists_finiteRestriction {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {S T : E →L[𝕜] F} (hfr : ∀ (n : ℕ) (ε : ℝ), 0 < ε → ∃ (v : Fin (n + 1) → E), (S + T).approximationNumber n < ((S + T) ∘SL (Submodule.span 𝕜 (Set.range v)).subtypeL).approximationNumber n + ε) (k : ℕ) : (S + T).kyFanGauge k ≤ S.kyFanGauge k + T.kyFanGauge k

Step 3 of the triangle inequality, and the only step that is not field-generic — so it takes the field-dependent input as a hypothesis.

Given that every approximation number of S + T is approached by its restrictions to finite-dimensional subspaces of the source, the Ky Fan triangle inequality for S and T follows: span the finitely many near-optimal vectors, restrict there, apply the finite-dimensional-source case, and let the tolerance go to zero.

Nothing else in the argument sees the scalars. Over ℂ the hypothesis is exists_finiteRestrictionApproximationNumber_add_gt, a corollary of the min-max theorem; over ℝ, where Mathlib's continuous functional calculus is not available for operators on the space itself, it is proved by complexification. Stating the step this way is what keeps the two fields from needing two copies of the argument.

theorem ContinuousLinearMap.kyFanGauge_add_le_of_hasMinMaxLowerBound {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (h : HasMinMaxLowerBound 𝕜 E F) (S T : E →L[𝕜] F) (k : ℕ) : (S + T).kyFanGauge k ≤ S.kyFanGauge k + T.kyFanGauge k

The Ky Fan triangle inequality over any scalar field with a min--max lower bound.

This is the general statement: kyFanGauge_add_le_of_exists_finiteRestriction needs a finite source restriction for every tolerance, and HasMinMaxLowerBound is exactly what produces one. The two concrete fields are corollaries — kyFanGauge_add_le_complex over ℂ below and TauCeti.ApproximationNumber.kyFanGauge_add_le_real over ℝ — and neither repeats any part of the argument.

theorem ContinuousLinearMap.exists_finiteRestrictionApproximationNumber_add_gt {E : Type v} {F : Type w} [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 + ε

Every positive tolerance admits a finite source restriction whose approximation number is within that tolerance of the ambient one, over ℂ.

theorem ContinuousLinearMap.kyFanGauge_add_le_complex {E : Type v} {F : Type w} [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, in full generality: arbitrary bounded operators between complex Hilbert spaces, no compactness or finite-dimensionality.

This is the inequality that makes every Ky Fan gauge a norm, and hence the one every symmetric operator ideal built on approximation numbers depends on. The argument is kyFanGauge_add_le_of_exists_finiteRestriction; what is complex-specific is only the min-max input it consumes.