Ky Fan's maximum principle and triangle inequality for approximation numbers

The Ky Fan gauge Kₖ(T) = a₀(T) + ⋯ + aₖ₋₁(T) of a bounded linear map T : E →L[𝕜] F is the sum of its first k approximation numbers. Between finite-dimensional inner product spaces it is the Ky Fan k-sum of singular values LinearMap.kyFanSum, by Eckart–Young, and so satisfies Ky Fan's triangle inequality Kₖ(S + T) ≤ Kₖ(S) + Kₖ(T).

This file carries the triangle inequality to inner product spaces of arbitrary dimension, on every pair E, F with the converse min–max localization property TauCeti.HasMinMaxLowerBound. On such a pair the first k approximation numbers of S + T are, up to any ε > 0, those of a compression of S + T to finite-dimensional subspaces V ≤ E and W ≤ F (TauCeti.HasMinMaxLowerBound.exists_singularValue_le_compression). Compressing S and T in the same way does not increase their approximation numbers, and the finite-dimensional Ky Fan inequality applies to the compressions. Every pair whose source space is complete has the localization property (TauCeti.HasMinMaxLowerBound.of_completeSpace), so the triangle inequality holds for bounded linear maps from a Hilbert space to an inner product space.

Ky Fan's maximum principle ‖∑ᵢ ⟪uᵢ, T vᵢ⟫‖ ≤ Kₖ(T), for orthonormal families (uᵢ) and (vᵢ) with k members, needs no localization: compressing T to the spans of the two families reduces it to the finite-dimensional principle LinearMap.norm_sum_inner_le_kyFanSum.

Main declarations

• ContinuousLinearMap.kyFanGauge_eq_kyFanSum: between finite-dimensional inner product spaces, Kₖ(T) is the Ky Fan k-sum of the singular values of T.
• ContinuousLinearMap.norm_sum_inner_le_kyFanGauge: Ky Fan's maximum principle, ‖∑ᵢ ⟪uᵢ, T vᵢ⟫‖ ≤ Kₖ(T) for orthonormal families (uᵢ), (vᵢ) with k members.
• TauCeti.HasMinMaxLowerBound.kyFanGauge_add_le: on a pair with the converse min–max localization property, Kₖ(S + T) ≤ Kₖ(S) + Kₖ(T).
• ContinuousLinearMap.kyFanGauge_add_le: Ky Fan triangle inequality, Kₖ(S + T) ≤ Kₖ(S) + Kₖ(T) for bounded linear maps on a complete inner product space.

References

• A. Pietsch, Eigenvalues and s-Numbers, Cambridge Studies in Advanced Mathematics 13, Cambridge University Press (1987), Chapter 2.
• I. C. Gohberg, M. G. Krein, Introduction to the Theory of Linear Nonselfadjoint Operators, Translations of Mathematical Monographs 18, AMS (1969), Chapter II, §4.

theorem ContinuousLinearMap.kyFanGauge_eq_kyFanSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) (k : ℕ) : ↑(T.kyFanGauge k) = (↑T).kyFanSum k

Eckart–Young for Ky Fan gauges. Between finite-dimensional inner product spaces, the Ky Fan gauge Kₖ(T) of a bounded linear map is the Ky Fan k-sum σ₀(T) + ⋯ + σₖ₋₁(T) of its singular values.

theorem ContinuousLinearMap.kyFanGauge_orthogonalProjectionOnto_comp_comp_subtypeL_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (W : Submodule 𝕜 F) [W.HasOrthogonalProjection] (V : Submodule 𝕜 E) (T : E →L[𝕜] F) (k : ℕ) : (W.orthogonalProjectionOnto ∘SL T ∘SL V.subtypeL).kyFanGauge k ≤ T.kyFanGauge k

Compressing a bounded linear map to subspaces of the source and target does not increase its Ky Fan gauges.

theorem ContinuousLinearMap.norm_sum_inner_le_kyFanGauge {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_4} [Fintype ι] (T : E →L[𝕜] F) {u : ι → F} {v : ι → E} (hu : Orthonormal 𝕜 u) (hv : Orthonormal 𝕜 v) : ‖∑ i : ι, inner 𝕜 (u i) (T (v i))‖ ≤ ↑(T.kyFanGauge (Fintype.card ι))

Ky Fan's maximum principle. For a bounded linear map T between inner product spaces and orthonormal families (uᵢ) in F and (vᵢ) in E with k members, ‖∑ᵢ ⟪uᵢ, T vᵢ⟫‖ ≤ a₀(T) + ⋯ + aₖ₋₁(T).

theorem TauCeti.HasMinMaxLowerBound.kyFanGauge_add_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [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

Ky Fan triangle inequality from the converse min–max localization. On a pair of inner product spaces with the property HasMinMaxLowerBound, the Ky Fan gauges are subadditive: Kₖ(S + T) ≤ Kₖ(S) + Kₖ(T).

theorem ContinuousLinearMap.kyFanGauge_add_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] (S T : E →L[𝕜] F) (k : ℕ) : (S + T).kyFanGauge k ≤ S.kyFanGauge k + T.kyFanGauge k

Ky Fan triangle inequality. For bounded linear maps from a complete inner product space to an inner product space, the Ky Fan gauges are subadditive: Kₖ(S + T) ≤ Kₖ(S) + Kₖ(T).