Hoffman–Wielandt inequality for singular values

For two linear maps with the same finite-dimensional domain and codomain, the squared Euclidean distance between their decreasingly ordered singular values is at most the squared Frobenius distance between the maps.

The proof uses the rectangular von Neumann trace inequality, obtained from a Ky Fan bound and summation by parts.

References

• J. von Neumann, Some matrix-inequalities and metrization of matric-space, Tomsk Univ. Rev. 1 (1937), 286–300.
• A. J. Hoffman and H. W. Wielandt, The variation of the spectrum of a normal matrix, Duke Math. J. 20 (1953), 37–39.
• L. Mirsky, Symmetric gauge functions and unitarily invariant norms, Quart. J. Math. 11 (1960), 50–59.
• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer (1997), Chapter IV.

theorem LinearMap.sum_sq_singularValues_sub_le_sq_frobenius_apply_sub_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] (A B : E →ₗ[𝕜] F) (hEF : Module.finrank 𝕜 E ≤ Module.finrank 𝕜 F) : ∑ i : Fin (Module.finrank 𝕜 E), (A.singularValues ↑i - B.singularValues ↑i) ^ 2 ≤ (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 E F) (A - B) ^ 2

The singular-value Hoffman–Wielandt inequality when the domain dimension does not exceed the codomain dimension. The squared distance between the ordered singular values is at most the squared Frobenius seminorm of the difference.

theorem LinearMap.sum_sq_singularValues_sub_le_sq_frobenius_apply_sub_min {𝕜 : 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) : ∑ i : Fin (min (Module.finrank 𝕜 E) (Module.finrank 𝕜 F)), (A.singularValues ↑i - B.singularValues ↑i) ^ 2 ≤ (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 E F) (A - B) ^ 2

The singular-value Hoffman–Wielandt inequality for arbitrary finite-dimensional maps. The sum runs over the first min (finrank 𝕜 E) (finrank 𝕜 F) singular values; beyond that index, both maps' singular values are zero.