The Hoffman–Wielandt inequality for Hermitian matrices

For Hermitian n × n matrices A and B over ℝ or ℂ, with eigenvalues λ₁(A) ≥ ⋯ ≥ λₙ(A) and λ₁(B) ≥ ⋯ ≥ λₙ(B) listed in decreasing order with multiplicity, the Hoffman–Wielandt inequality bounds the Euclidean distance between the sorted spectra by the Frobenius distance between the matrices:

∑ᵢ (λᵢ(A) - λᵢ(B))² ≤ ‖A - B‖_F².

This is the matrix form of the operator inequality LinearMap.IsSymmetric.sum_sq_eigenvalues_sub_le_sum_sq_norm_apply, applied to Matrix.toEuclideanLin A and Matrix.toEuclideanLin B in the standard orthonormal basis. The Frobenius norm is Mathlib's Matrix.frobeniusNormedAddCommGroup, available through open scoped Matrix.Norms.Frobenius.

Combined with the Cauchy–Schwarz inequality it shows that integrals of Lipschitz functions against empirical spectral measures are Lipschitz in the matrix: if f is K-Lipschitz, then

‖∫ f dL_A - ∫ f dL_B‖ ≤ K ‖A - B‖_F / √n.

This is the deterministic estimate behind truncation and concentration arguments for random matrices: a perturbation of small Frobenius norm hardly moves linear spectral statistics, and the map A ↦ ∫ f dL_A is a Lipschitz function of the matrix entries.

Main results

• Matrix.IsHermitian.sum_sq_eigenvalues₀_sub_le_frobenius_norm_sub_sq: the Hoffman–Wielandt inequality ∑ᵢ (λᵢ(A) - λᵢ(B))² ≤ ‖A - B‖_F².
• Matrix.sum_sq_singularValues_toEuclideanLin_sub_le_frobenius_norm_sub_sq: the rectangular singular-value Hoffman–Wielandt inequality.
• Matrix.norm_integral_spectralMeasure_sub_integral_spectralMeasure_le: for a K-Lipschitz f, ‖∫ f dL_A - ∫ f dL_B‖ ≤ K ‖A - B‖_F / √n.

References

• A. J. Hoffman, H. W. Wielandt, The variation of the spectrum of a normal matrix, Duke Math. J. 20 (1953), 37–39.
• G. W. Anderson, A. Guionnet, O. Zeitouni, An Introduction to Random Matrices, Cambridge University Press (2010), Lemma 2.1.19 and §2.3.1.

theorem Matrix.sum_sq_singularValues_toEuclideanLin_sub_le_frobenius_norm_sub_sq {m : Type u_3} {n : Type u_4} [Fintype m] [Fintype n] [DecidableEq n] {𝕜 : Type u_5} [RCLike 𝕜] (A B : Matrix m n 𝕜) : ∑ i : Fin (min (Fintype.card n) (Fintype.card m)), ((toEuclideanLin A).singularValues ↑i - (toEuclideanLin B).singularValues ↑i) ^ 2 ≤ ‖A - B‖ ^ 2

The singular-value Hoffman–Wielandt inequality for same-shaped rectangular matrices: the squared distance between their ordered singular values, summed up to the smaller dimension, is bounded by the squared Frobenius norm of their difference.

theorem Matrix.IsHermitian.sum_sq_eigenvalues₀_sub_le_frobenius_norm_sub_sq {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A B : Matrix n n 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) : ∑ i : Fin (Fintype.card n), (hA.eigenvalues₀ i - hB.eigenvalues₀ i) ^ 2 ≤ ‖A - B‖ ^ 2

The Hoffman–Wielandt inequality for Hermitian matrices: the squared Euclidean distance between the decreasingly sorted spectra is at most the squared Frobenius norm ‖A - B‖_F².

theorem Matrix.norm_integral_spectralMeasure_sub_integral_spectralMeasure_le {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A B : Matrix n n 𝕜} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [Nonempty n] (hA : A.IsHermitian) (hB : B.IsHermitian) {K : NNReal} {f : ℝ → E} (hf : LipschitzWith K f) : ‖∫ (x : ℝ), f x ∂↑(A.spectralMeasure hA) - ∫ (x : ℝ), f x ∂↑(B.spectralMeasure hB)‖ ≤ ↑K * ‖A - B‖ / √↑(Fintype.card n)

Integrals of a K-Lipschitz function against empirical spectral measures are Lipschitz in the matrix: ‖∫ f dL_A - ∫ f dL_B‖ ≤ K ‖A - B‖_F / √n, for Hermitian A and B of size n.