The Ky Fan and nuclear seminorms

For linear maps A : E →ₗ[𝕜] F between finite-dimensional inner product spaces, the Ky Fan k-sum A.kyFanSum k = σ₀(A) + ⋯ + σₖ₋₁(A) of the k largest singular values is subadditive (LinearMap.kyFanSum_add_le), absolutely homogeneous (LinearMap.kyFanSum_smul) and invariant under isometric changes of coordinates. It is therefore a unitarily invariant seminorm, the Ky Fan k-seminorm. The sum of all singular values is the nuclear seminorm (the trace norm); it is the Ky Fan k-seminorm for every k at least the rank of A.

These are the seminorms through which Fan dominance (TauCeti.UnitarilyInvariantSeminorm.map_le_of_kyFanSum_le) is stated: Ky Fan domination is domination in every Ky Fan seminorm.

Main declarations

• TauCeti.UnitarilyInvariantSeminorm.kyFan: the Ky Fan k-seminorm A ↦ A.kyFanSum k.
• TauCeti.UnitarilyInvariantSeminorm.nuclear: the nuclear seminorm, the sum of all singular values.
• TauCeti.UnitarilyInvariantSeminorm.nuclear_apply: N₁(A) = ∑ᵢ σᵢ(A).
• LinearMap.kyFanSum_eq_nuclear: the Ky Fan sums stabilize at the nuclear seminorm from the rank on.

References

• K. Fan, Maximum properties and inequalities for the eigenvalues of completely continuous operators, Proc. Nat. Acad. Sci. U.S.A. 37 (1951), 760–766.
• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer, 1997, Section IV.2.

noncomputable def TauCeti.UnitarilyInvariantSeminorm.kyFan (𝕜 : 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 : ℕ) : UnitarilyInvariantSeminorm 𝕜 E F

The Ky Fan k-seminorm A ↦ σ₀(A) + ⋯ + σₖ₋₁(A), the sum of the k largest singular values, as a unitarily invariant seminorm.

noncomputable def TauCeti.UnitarilyInvariantSeminorm.nuclear (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] : UnitarilyInvariantSeminorm 𝕜 E F

The nuclear seminorm (trace norm) A ↦ ∑ᵢ σᵢ(A), the sum of all singular values, as a unitarily invariant seminorm. It is the Ky Fan k-seminorm for k = finrank 𝕜 E, beyond which all singular values vanish.

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.kyFan_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] (k : ℕ) (A : E →ₗ[𝕜] F) : (kyFan 𝕜 E F k) A = A.kyFanSum k

The k-th Ky Fan seminorm evaluates to the sum σ₀(A) + ⋯ + σₖ₋₁(A) of the k largest singular values.

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.nuclear_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 : E →ₗ[𝕜] F) : (nuclear 𝕜 E F) A = A.singularValues.sum fun (x : ℕ) (s : ℝ) => s

The nuclear seminorm is the sum of all singular values.

theorem LinearMap.kyFanSum_eq_nuclear {𝕜 : 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 : Module.finrank 𝕜 ↥A.range ≤ k) : A.kyFanSum k = (TauCeti.UnitarilyInvariantSeminorm.nuclear 𝕜 E F) A

From the rank on, the Ky Fan sums are the nuclear seminorm: if rank A ≤ k, then σ₀(A) + ⋯ + σₖ₋₁(A) = ∑ᵢ σᵢ(A).