feat: add Lidskii–Last eigenvalue-perturbation eval problem

LeanEval/LinearAlgebra/Lidskii.lean

@@ -0,0 +1,37 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace LinearAlgebra
+
+/-!
+# Lidskii–Last eigenvalue-perturbation theorem
+
+§99 of Oliver Knill's *Some Fundamental Theorems in Mathematics*. For two
+self-adjoint complex `n × n` matrices `A, B` with eigenvalues sorted in the
+same order, the total eigenvalue displacement is bounded by the entrywise
+`ℓ¹` distance:
+
+  `∑ⱼ |αⱼ − βⱼ| ≤ ∑ᵢⱼ |Aᵢⱼ − Bᵢⱼ|`.
+
+This is Last's theorem (≈ 1993), a consequence of Lidskii's inequality
+(1950). mathlib has `Matrix.IsHermitian.eigenvalues₀` (the spectral-theorem
+eigenvalues) but none of the classical eigenvalue-perturbation bounds
+(Lidskii, Ky Fan, Hoffman–Wielandt). The statement needs no auxiliary
+definitions.
+-/
+
+open Matrix
+
+/-- **Lidskii–Last theorem.** For two self-adjoint complex `n × n` matrices
+`A, B`, with eigenvalues sorted in the same order,
+`∑ⱼ |αⱼ − βⱼ| ≤ ∑ᵢⱼ |Aᵢⱼ − Bᵢⱼ|`. -/
+@[eval_problem]
+theorem lidskii_last {n : Type*} [Fintype n] [DecidableEq n]
+    {A B : Matrix n n ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) :
+    ∑ j, |hA.eigenvalues₀ j - hB.eigenvalues₀ j| ≤
+      ∑ i, ∑ j, ‖A i j - B i j‖ := by
+  sorry
+
+end LinearAlgebra
+end LeanEval

manifests/problems.toml

@@ -673,3 +673,14 @@ module = "LeanEval.Geometry.Uniformization"
 holes = ["uniformization"]
 submitter = "Junyan Xu"
 source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, Chapter 1."
+
+[[problem]]
+id = "lidskii_last"
+title = "Lidskii–Last eigenvalue-perturbation theorem"
+test = false
+module = "LeanEval.LinearAlgebra.Lidskii"
+holes = ["lidskii_last"]
+submitter = "Kim Morrison"
+notes = "§99 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. For two self-adjoint complex n×n matrices A, B with eigenvalues sorted in the same order, the total eigenvalue displacement ∑|α_j - β_j| is bounded by the entrywise ℓ¹ distance ∑|A_ij - B_ij|. This is Last's theorem (≈1993), a consequence of Lidskii's inequality (1950). Uses Matrix.IsHermitian.eigenvalues₀; mathlib has no Lidskii, Ky Fan, or Hoffman-Wielandt perturbation bounds, and no formalization of the theorem was found in any other proof assistant."
+source = "V. B. Lidskii (1950); the entrywise ℓ¹ form is due to Y. Last (around 1993). Listed as §99 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf)."
+informal_solution = "By Lidskii's inequality the vector of sorted-eigenvalue displacements of A and B is majorized by the vector of eigenvalues of C := B - A (proved via the Ky Fan extremal characterization of partial sums of eigenvalues), so ∑_j |α_j - β_j| ≤ ∑_j |γ_j| with γ the eigenvalues of C. Then ∑_j |γ_j| ≤ ∑_{i,j} |C_ij|: for Hermitian C the ℓ¹ norm of the eigenvalues is dominated by the ℓ¹ norm of the matrix entries (bound each |γ_j| using the spectral decomposition and the triangle inequality). Combining the two gives the entrywise bound."