Wasserstein bounds for empirical spectral measures

Pair the decreasingly sorted eigenvalues of two Hermitian matrices, with multiplicity, to couple their empirical spectral measures. The quadratic cost of this coupling is the average squared displacement of the sorted eigenvalues. The Hoffman–Wielandt inequality therefore gives

W₂(L_A, L_B) ≤ ‖A - B‖_F / √(card n).

The same estimate holds for W₁ by monotonicity in the exponent. These bounds transfer small Frobenius perturbations of matrices to small transport distances between their spectral laws, with the dimension normalization needed for truncation arguments in global spectral limits. The norms in this file are Frobenius norms, through Matrix.Norms.Frobenius.

The construction reuses TauCeti.Probability.empiricalMeasureOfFintype; the matrix inequality is Matrix.IsHermitian.sum_sq_eigenvalues₀_sub_le_frobenius_norm_sub_sq.

References

• G. W. Anderson, A. Guionnet, O. Zeitouni, An Introduction to Random Matrices, Cambridge University Press (2010), Lemma 2.1.19 and §2.3.1.

noncomputable def Matrix.spectralCoupling {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] [RCLike 𝕜] (A B : Matrix n n 𝕜) (hA : A.IsHermitian) (hB : B.IsHermitian) : MeasureTheory.ProbabilityMeasure (ℝ × ℝ)

The empirical coupling pairing the decreasingly sorted eigenvalues of A and B, with mass 1 / card n at each pair, counted with multiplicity.

theorem Matrix.spectralCoupling_def {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] [RCLike 𝕜] (A B : Matrix n n 𝕜) (hA : A.IsHermitian) (hB : B.IsHermitian) : A.spectralCoupling B hA hB = TauCeti.Probability.empiricalMeasureOfFintype fun (i : Fin (Fintype.card n)) => (hA.eigenvalues₀ i, hB.eigenvalues₀ i)

The spectral coupling is the empirical law of the sorted eigenvalue pairs.

@[simp]

theorem Matrix.fst_spectralCoupling {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] [RCLike 𝕜] (A B : Matrix n n 𝕜) (hA : A.IsHermitian) (hB : B.IsHermitian) : (↑(A.spectralCoupling B hA hB)).fst = ↑(A.spectralMeasure hA)

The first marginal of the sorted spectral coupling is the spectral measure of A.

@[simp]

theorem Matrix.snd_spectralCoupling {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] [RCLike 𝕜] (A B : Matrix n n 𝕜) (hA : A.IsHermitian) (hB : B.IsHermitian) : (↑(A.spectralCoupling B hA hB)).snd = ↑(B.spectralMeasure hB)

The second marginal of the sorted spectral coupling is the spectral measure of B.

theorem Matrix.isCoupling_spectralCoupling {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] [RCLike 𝕜] (A B : Matrix n n 𝕜) (hA : A.IsHermitian) (hB : B.IsHermitian) : TauCeti.IsCoupling ↑(A.spectralCoupling B hA hB) ↑(A.spectralMeasure hA) ↑(B.spectralMeasure hB)

Pairing sorted eigenvalues gives a coupling of the two spectral measures.

theorem Matrix.lintegral_spectralCoupling {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] [RCLike 𝕜] (A B : Matrix n n 𝕜) (hA : A.IsHermitian) (hB : B.IsHermitian) {f : ℝ × ℝ → ENNReal} : ∫⁻ (z : ℝ × ℝ), f z ∂↑(A.spectralCoupling B hA hB) = (↑(Fintype.card n))⁻¹ * ∑ i : Fin (Fintype.card n), f (hA.eigenvalues₀ i, hB.eigenvalues₀ i)

Integrating a nonnegative cost against the sorted spectral coupling averages the cost of the corresponding eigenvalue pairs.

theorem Matrix.lintegral_edist_sq_spectralCoupling {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] [RCLike 𝕜] (A B : Matrix n n 𝕜) (hA : A.IsHermitian) (hB : B.IsHermitian) : ∫⁻ (z : ℝ × ℝ), edist z.1 z.2 ^ 2 ∂↑(A.spectralCoupling B hA hB) = ENNReal.ofReal ((↑(Fintype.card n))⁻¹ * ∑ i : Fin (Fintype.card n), (hA.eigenvalues₀ i - hB.eigenvalues₀ i) ^ 2)

The quadratic transport cost of the sorted spectral coupling is the mean squared sorted eigenvalue displacement.

theorem Matrix.wassersteinEDist_two_spectralMeasure_sq_le {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] [RCLike 𝕜] (A B : Matrix n n 𝕜) (hA : A.IsHermitian) (hB : B.IsHermitian) : TauCeti.wassersteinEDist 2 ↑(A.spectralMeasure hA) ↑(B.spectralMeasure hB) ^ 2 ≤ ENNReal.ofReal (‖A - B‖ ^ 2 / ↑(Fintype.card n))

Spectral Wasserstein bound, squared form. The squared W₂ distance between the empirical spectral measures is at most the normalized squared Frobenius distance.

theorem Matrix.wassersteinEDist_two_spectralMeasure_le {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] [RCLike 𝕜] (A B : Matrix n n 𝕜) (hA : A.IsHermitian) (hB : B.IsHermitian) : TauCeti.wassersteinEDist 2 ↑(A.spectralMeasure hA) ↑(B.spectralMeasure hB) ≤ ENNReal.ofReal (‖A - B‖ / √↑(Fintype.card n))

Spectral W₂ bound. A Frobenius perturbation of size ε moves the empirical spectral measure by at most ε / √(card n) in quadratic Wasserstein distance.

theorem Matrix.wassersteinEDist_one_spectralMeasure_le {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] [RCLike 𝕜] (A B : Matrix n n 𝕜) (hA : A.IsHermitian) (hB : B.IsHermitian) : TauCeti.wassersteinEDist 1 ↑(A.spectralMeasure hA) ↑(B.spectralMeasure hB) ≤ ENNReal.ofReal (‖A - B‖ / √↑(Fintype.card n))

Spectral W₁ bound. The normalized Frobenius bound also controls the linear Wasserstein distance between empirical spectral measures.