Ky Fan sums of singular values

For operators on finite-dimensional inner product spaces over 𝕜 = ℝ, ℂ:

• kyFanSum k A = ∑_{i<k} σᵢ(A), the Ky Fan k-sums;
• the Ky Fan trace inequality: for a symmetric S and an orthonormal family w : Fin k → E, ∑ᵢ re⟪S wᵢ, wᵢ⟫ ≤ ∑_{i<k} λᵢ(S);
• the Ky Fan variational principle: kyFanSum k A is the maximum of re ∑ᵢ ⟪uᵢ, A vᵢ⟫ over orthonormal k-families u, v;
• weak majorization kyFanSum k (A + B) ≤ kyFanSum k A + kyFanSum k B — the triangle inequality for every Ky Fan norm simultaneously, the engine of the Fan dominance principle (UnitarilyInvariantSeminorm.lean);
• unitary invariance, adjoint invariance, and nonnegative-real scaling of singular values and Ky Fan sums, plus the bounded-factor domination σᵢ(C ∘ A) ≤ c σᵢ(A) (Loewner monotonicity of the Gram eigenvalues).

References

• R. Bhatia, Matrix Analysis, Chapter IV (Ky Fan norms, dominance).
• K. Fan, On a theorem of Weyl concerning eigenvalues of linear transformations I, Proc. Nat. Acad. Sci. USA 35 (1949), 652–655.

Singular values under unitaries, scaling, and bounded factors (F0)

theorem TauCeti.singularValues_unitary_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (U : F ≃ₗᵢ[𝕜] F) (A : E →ₗ[𝕜] F) : (↑U.toLinearEquiv ∘ₗ A).singularValues = A.singularValues

Post-composing with a unitary does not change the singular values.

theorem TauCeti.singularValues_comp_unitary {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (U : E ≃ₗᵢ[𝕜] E) : (A ∘ₗ ↑U.toLinearEquiv).singularValues = A.singularValues

Pre-composing with a unitary does not change the singular values.

theorem TauCeti.isSymmetric_real_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {S : E →ₗ[𝕜] E} (hS : S.IsSymmetric) (r : ℝ) : (↑r • S).IsSymmetric

Real-smul of a symmetric operator is symmetric.

theorem TauCeti.eigenvalues_real_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {S : E →ₗ[𝕜] E} (hS : S.IsSymmetric) {n : ℕ} (hn : Module.finrank 𝕜 E = n) {r : ℝ} (hr : 0 ≤ r) : ⋯.eigenvalues hn = fun (i : Fin n) => r * hS.eigenvalues hn i

Sorted eigenvalues scale under a nonnegative real scaling.

theorem TauCeti.singularValues_real_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {r : ℝ} (hr : 0 ≤ r) (i : ℕ) : (↑r • A).singularValues i = r * A.singularValues i

Singular values scale by r under a nonnegative real scaling.

theorem TauCeti.singularValues_comp_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {F' : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] [NormedAddCommGroup F'] [InnerProductSpace 𝕜 F'] [FiniteDimensional 𝕜 F'] {C : F →ₗ[𝕜] F'} {c : ℝ} (hc : 0 ≤ c) (hC : ∀ (y : F), ‖C y‖ ≤ c * ‖y‖) (A : E →ₗ[𝕜] F) (i : ℕ) : (C ∘ₗ A).singularValues i ≤ c * A.singularValues i

Domination by a bounded left factor: σᵢ(C ∘ A) ≤ c σᵢ(A) when ‖C y‖ ≤ c ‖y‖. Via Loewner monotonicity of the Gram eigenvalues.

theorem TauCeti.singularValues_comp_le' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {X : E →ₗ[𝕜] F} {C : E →ₗ[𝕜] E} {c : ℝ} (hc : 0 ≤ c) (hC : ∀ (y : E), ‖C y‖ ≤ c * ‖y‖) (i : ℕ) : (X ∘ₗ C).singularValues i ≤ c * X.singularValues i

Domination by a bounded right factor: σᵢ(X ∘ C) ≤ c σᵢ(X). Via singularValues_adjoint.

theorem TauCeti.eigenvalues_operatorAbs {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : ⋯.eigenvalues ⋯ = fun (i : Fin (Module.finrank 𝕜 E)) => A.singularValues ↑i

The sorted eigenvalues of the modulus |A| are the singular values.

The Ky Fan trace inequality (F1.a–b)

theorem TauCeti.sum_re_inner_le_sum_eigenvalues_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {S : E →ₗ[𝕜] E} (hS : S.IsSymmetric) {n : ℕ} (hn : Module.finrank 𝕜 E = n) {k : ℕ} (hk : k ≤ n) {w : Fin k → E} (hw : Orthonormal 𝕜 w) : ∑ i : Fin k, RCLike.re (inner 𝕜 (S (w i)) (w i)) ≤ ∑ j : Fin n with ↑j < k, hS.eigenvalues hn j

The Ky Fan trace inequality. For a symmetric operator S and an orthonormal family w : Fin k → E, ∑ᵢ re ⟪S (w i), w i⟫ ≤ ∑_{j < k} λⱼ(S) — the trace of S compressed to any k-dimensional subspace is at most the sum of the k largest eigenvalues. (Ky Fan's maximum principle; implies the Schur–Horn partial-sum inequalities.)

The Ky Fan variational principle (F1.c)

theorem TauCeti.sum_filter_lt_eq_sum_fin {n k : ℕ} (hk : k ≤ n) (f : ℕ → ℝ) : ∑ j : Fin n with ↑j < k, f ↑j = ∑ i : Fin k, f ↑i

Index plumbing: a top-k filtered sum over Fin n is a sum over Fin k. (Not private: UnitarilyInvariantSeminorm.lean consumes it to convert kyFanSum domination into the prefix-sum hypothesis of the T-transform descent.)

Ky Fan sums and weak majorization (F2)

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib.Analysis.InnerProductSpace.KyFan, moved to ForTauCeti in the Wave-1 staging migration; introduced at Davis--Kahan commit 199390a.
• Extraction class: moved. The Wave-1 migration renamed the namespace ForMathlib to TauCeti; declaration names and proofs are unchanged.
• Original authors / copyright: Jon Crall, Claude Fable 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib and sibling ForTauCeti staging modules.

noncomputable def TauCeti.kyFanSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (k : ℕ) (A : E →ₗ[𝕜] F) : ℝ

The Ky Fan k-sum of an operator: the sum of its k largest singular values. kyFanSum 1 A = ‖A‖, kyFanSum (finrank 𝕜 E) A is the trace norm.

The enclosing exposed public section keeps the defining sum visible across module boundaries for the rfl-level rewrites in the Ky Fan and unitarily-invariant-norm development.

Equations

• TauCeti.kyFanSum k A = ∑ i : Fin k, A.singularValues ↑i

theorem TauCeti.kyFanSum_eq_sum_fin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (k : ℕ) (A : E →ₗ[𝕜] F) : kyFanSum k A = ∑ i : Fin k, A.singularValues ↑i

The Ky Fan sum as a finite singular-value vector sum.

theorem TauCeti.kyFanSum_eq_sum_range {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (k : ℕ) (A : E →ₗ[𝕜] F) : kyFanSum k A = ∑ i ∈ Finset.range k, A.singularValues i

The Ky Fan sum as the sum over the natural-number prefix [0, k).

theorem TauCeti.kyFanSum_nonneg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (k : ℕ) (A : E →ₗ[𝕜] F) : 0 ≤ kyFanSum k A

Ky Fan sums are nonnegative, being sums of singular values.

theorem TauCeti.kyFanSum_eq_of_finrank_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {k : ℕ} (hk : Module.finrank 𝕜 E ≤ k) (A : E →ₗ[𝕜] F) : kyFanSum k A = kyFanSum (Module.finrank 𝕜 E) A

Ky Fan sums saturate at k = finrank: larger k adds only zeros.

theorem TauCeti.kyFanSum_add_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (k : ℕ) (A B : E →ₗ[𝕜] F) : kyFanSum k (A + B) ≤ kyFanSum k A + kyFanSum k B

The Ky Fan triangle inequality for arbitrary rectangular maps and every prefix length.

theorem TauCeti.kyFanSum_le_of_singularValues_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A B : E →ₗ[𝕜] F} (h : ∀ (i : ℕ), A.singularValues i ≤ B.singularValues i) (k : ℕ) : kyFanSum k A ≤ kyFanSum k B

Pointwise singular-value domination gives Ky Fan domination.

theorem TauCeti.kyFanSum_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (k : ℕ) (A : E →ₗ[𝕜] F) : kyFanSum k (LinearMap.adjoint A) = kyFanSum k A

Ky Fan sums are adjoint-invariant, since the singular values are.

theorem TauCeti.kyFanSum_unitary_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (k : ℕ) (U : F ≃ₗᵢ[𝕜] F) (A : E →ₗ[𝕜] F) : kyFanSum k (↑U.toLinearEquiv ∘ₗ A) = kyFanSum k A

Ky Fan sums are unchanged by a unitary on the codomain.

theorem TauCeti.kyFanSum_comp_unitary {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (k : ℕ) (A : E →ₗ[𝕜] F) (U : E ≃ₗᵢ[𝕜] E) : kyFanSum k (A ∘ₗ ↑U.toLinearEquiv) = kyFanSum k A

Ky Fan sums are unchanged by a unitary on the domain. With kyFanSum_unitary_comp this is the two-sided unitary invariance that makes each Ky Fan sum a unitarily invariant norm.

theorem TauCeti.kyFanSum_real_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (k : ℕ) (A : E →ₗ[𝕜] F) {r : ℝ} (hr : 0 ≤ r) : kyFanSum k (↑r • A) = r * kyFanSum k A

Ky Fan sums are absolutely homogeneous under real scaling.

theorem TauCeti.singularValues_smul_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (a : 𝕜) (A : E →ₗ[𝕜] F) (i : ℕ) : (a • A).singularValues i = ‖a‖ * A.singularValues i

Singular values scale by the norm of an arbitrary scalar.

theorem TauCeti.singularValues_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (a : 𝕜) (A : E →ₗ[𝕜] F) : (a • A).singularValues = ‖a‖ • A.singularValues

Bundled singular-value sequence of a scalar multiple. This is the Finsupp-level companion to singularValues_smul_apply; it is convenient when a unitarily invariant norm is compared through its complete gauge sequence.

theorem TauCeti.re_sum_inner_map_le_kyFanSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] F} {k : ℕ} (hk : k ≤ Module.finrank 𝕜 E) {u : Fin k → F} {v : Fin k → E} (hu : Orthonormal 𝕜 u) (hv : Orthonormal 𝕜 v) : RCLike.re (∑ i : Fin k, inner 𝕜 (u i) (A (v i))) ≤ kyFanSum k A

Rectangular Ky Fan variational principle, upper bound.

For orthonormal domain and codomain families, the real part of the paired matrix coefficient sum is bounded by the corresponding singular-value prefix. The proof embeds both families in the two coordinates of the L² product and applies the square Ky Fan variational principle to zeroExtension A.

theorem TauCeti.sum_le_kyFanSum_of_orthonormal {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] F} {k : ℕ} (hk : k ≤ Module.finrank 𝕜 E) {u : Fin k → F} {v : Fin k → E} (hu : Orthonormal 𝕜 u) (hv : Orthonormal 𝕜 v) {t : Fin k → ℝ} (ht : ∀ (i : Fin k), t i ≤ RCLike.re (inner 𝕜 (u i) (A (v i)))) : ∑ i : Fin k, t i ≤ kyFanSum k A

A convenient witness form of the rectangular Ky Fan upper bound.

theorem TauCeti.orthonormal_unimodular_smul {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_5} {u : ι → F} (hu : Orthonormal 𝕜 u) {c : ι → 𝕜} (hc : ∀ (i : ι), ‖c i‖ = 1) : Orthonormal 𝕜 fun (i : ι) => c i • u i

Rescaling an orthonormal family by unimodular scalars leaves it orthonormal.

theorem TauCeti.sum_abs_le_kyFanSum_of_orthonormal {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] F} {k : ℕ} (hk : k ≤ Module.finrank 𝕜 E) {u : Fin k → F} {v : Fin k → E} (hu : Orthonormal 𝕜 u) (hv : Orthonormal 𝕜 v) {t : Fin k → ℝ} (ht : ∀ (i : Fin k), t i ≤ |RCLike.re (inner 𝕜 (u i) (A (v i)))|) : ∑ i : Fin k, t i ≤ kyFanSum k A

Absolute-value witness form of the rectangular Ky Fan upper bound. Because the two orthonormal families may be rephased independently, the Ky Fan prefix dominates the sum of the magnitudes of the matched coefficients, not merely their signed real parts. This is the form needed whenever the sign of each matched coefficient is dictated by the geometry rather than chosen.

theorem TauCeti.exists_orthonormal_re_sum_inner_map_eq_kyFanSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {k : ℕ} (hkE : k ≤ Module.finrank 𝕜 E) (hkF : k ≤ Module.finrank 𝕜 F) : ∃ (u : Fin k → F) (v : Fin k → E), Orthonormal 𝕜 u ∧ Orthonormal 𝕜 v ∧ RCLike.re (∑ i : Fin k, inner 𝕜 (u i) (A (v i))) = kyFanSum k A

Rectangular Ky Fan variational principle, achievability.

For A : E →ₗ[𝕜] F between finite-dimensional inner product spaces and any k no larger than either dimension, the upper bound re_sum_inner_map_le_kyFanSum is attained: there are orthonormal k-families v in the domain and u in the codomain with re ∑ᵢ ⟪uᵢ, A vᵢ⟫ = ∑_{i<k} σᵢ(A).

Both dimension hypotheses are needed, and neither is an artefact of the proof: the statement asserts the existence of orthonormal k-tuples in E and in F, so it is false as soon as k exceeds either dimension.

The domain family is read off the eigenbasis of A⋆A, exactly as in the square case exists_orthonormal_re_sum_inner_map_eq_square. The codomain family cannot be obtained from a unitary the way the square case obtains it from the polar factor, because A need not have one; instead the normalized images σᵢ⁻¹ • A vᵢ of the directions with σᵢ ≠ 0 are an orthonormal family in F, and Orthonormal.exists_orthonormalBasis_extension_of_card_eq completes it. The directions with σᵢ = 0 contribute nothing to either side, since ‖A vᵢ‖ = σᵢ.