The Eckart–Young theorem: approximation numbers are singular values

For a bounded linear map T : E →L[𝕜] F between finite-dimensional inner product spaces over ℝ or ℂ, the approximation number aₙ(T), the distance from T to the maps of rank at most n, is the n-th singular value σₙ(T) = (T : E →ₗ[𝕜] F).singularValues n, including the zero tail from the dimension of E on. This identifies the approximation numbers, which make sense for operators between arbitrary normed spaces, with the singular values of finite-dimensional linear algebra, so estimates proved for either sequence transfer to the other.

Let (vᵢ) be the right singular basis of T, the orthonormal eigenbasis of T† T in which T† T vᵢ = σᵢ² vᵢ. Projecting away from the span of the vᵢ with i < n gives an approximant of rank at most n whose error is T restricted to the span of the vᵢ with i ≥ n, of norm at most σₙ; this is the orthogonal-tail bound ContinuousLinearMap.singularValue_le_nnnorm_comp_orthogonal. Conversely T stretches every vector of the (n + 1)-dimensional span of the vᵢ with i ≤ n by at least σₙ, so σₙ ≤ aₙ(T) by the coercive-subspace bound ContinuousLinearMap.le_singularValue_of_lt_rank.

Two consequences are recorded for linear maps: the operator norm is the largest singular value, and singular values are 1-Lipschitz in the operator norm (Weyl's perturbation bound for singular values), transferred from the corresponding facts a₀(T) = ‖T‖ and |aₙ(S) - aₙ(T)| ≤ ‖S - T‖.

Main declarations

• ContinuousLinearMap.singularValue_eq_linearMap_singularValues: Eckart–Young, aₙ(T) = σₙ(T) in finite dimension.
• LinearMap.norm_toContinuousLinearMap_eq_singularValues_zero: ‖A‖ = σ₀(A).
• LinearMap.abs_singularValues_sub_singularValues_le: |σₙ(A) - σₙ(B)| ≤ ‖A - B‖.

References

• C. Eckart, G. Young, The approximation of one matrix by another of lower rank, Psychometrika 1 (1936), 211–218.
• R. A. Horn, C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press (2013), Chapter 7 (the singular value decomposition and its consequences).
• A. Pietsch, Eigenvalues and s-Numbers, Cambridge Studies in Advanced Mathematics 13, Cambridge University Press (1987), Chapter 2.

theorem ContinuousLinearMap.singularValue_eq_linearMap_singularValues {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : ↑(T.singularValue n) = (↑T).singularValues n

Eckart–Young. Between finite-dimensional inner product spaces, the approximation numbers of a bounded linear map are its singular values: aₙ(T) = σₙ(T) for every n, both sides vanishing from the dimension of the source on.

theorem LinearMap.norm_toContinuousLinearMap_eq_singularValues_zero {𝕜 : 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) : ‖toContinuousLinearMap A‖ = A.singularValues 0

The operator norm of a linear map between finite-dimensional inner product spaces is its largest singular value: ‖A‖ = σ₀(A).

theorem LinearMap.abs_singularValues_sub_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) (n : ℕ) : |A.singularValues n - B.singularValues n| ≤ ‖toContinuousLinearMap (A - B)‖

Weyl's perturbation bound for singular values. Each singular value of a linear map between finite-dimensional inner product spaces is 1-Lipschitz in the operator norm: |σₙ(A) - σₙ(B)| ≤ ‖A - B‖.