Hoffman-Wielandt Inequality (1953)

For two m × n real matrices A, B with ordered singular values, the sum of squared differences between corresponding singular values is bounded by the squared Frobenius norm of their difference.

theorem hoffman_wielandt_inequality {d T : ℕ} (A B : Matrix (Fin d) (Fin T) ℝ) (S_A : SVD d T) (hA : S_A.IsDecompOf A) (hA_ord : S_A.IsOrdered) (S_B : SVD d T) (hB : S_B.IsDecompOf B) (hB_ord : S_B.IsOrdered) (hr : S_A.r = S_B.r) : ∑ k : Fin S_A.r, |S_A.σval k - S_B.σval (Fin.cast hr k)| ^ 2 ≤ ‖A - B‖ ^ 2

Hoffman-Wielandt inequality (1953). Stated without proof in the textbook. The standard proof requires Von Neumann's trace inequality which is not available in Mathlib.

For two m × n matrices A and B with SVD decompositions having the same number of components r and singular values in non-increasing order:

Σ_k |σ_k(A) - σ_k(B)|² ≤ ‖A - B‖_F²

This is stronger than Weyl's inequality (which bounds the max rather than the sum), but uses the Frobenius norm instead of the operator norm.

In the book (Rigollet, High Dimensional Statistics, Section 4.1), this is stated without proof as a standard result in matrix perturbation theory.

Why this is an axiom. The textbook states this without proof, and a formalized proof requires infrastructure not available in Mathlib4 as of 2025:

1. Von Neumann trace inequality: tr(AᵀB) ≤ Σ_k σ_k(A)σ_k(B) when singular values are in decreasing order. This is the key ingredient that gives the tight bound (as opposed to r copies of the Weyl bound, which is too weak by a factor of r).

2. Unitary invariance of the Frobenius norm: ‖UAV‖_F = ‖A‖_F for orthogonal U, V. Mathlib defines the Frobenius norm (Matrix.frobeniusNormedAddCommGroup) but does not provide this invariance lemma.

3. Orthonormality of SVD vectors: the SVD structure does not enforce that singular vectors are orthonormal, which is needed for the Frobenius norm identity ‖M‖_F² = Σ_k σ_k(M)².

The standard proof (Hoffman–Wielandt, 1953) proceeds as follows:

• Write ‖A - B‖_F² = Tr((A - B)ᵀ(A - B)).
• Substitute the SVDs A = U_A Σ_A V_Aᵀ and B = U_B Σ_B V_Bᵀ.
• Use unitary invariance to reduce to Tr(Σ_A² + Σ_B² - 2Σ_A Oᵀ Σ_B O) where O is an orthogonal matrix.
• Apply the rearrangement inequality to show that the cross term Tr(Σ_A Oᵀ Σ_B O) ≤ Σ_k σ_k(A)σ_k(B), yielding the result.

Reference: A.J. Hoffman and H.W. Wielandt, "The variation of the spectrum of a normal matrix," Duke Math. J., 20(1):37–39, 1953.