From f62afb8f13f82be120f9409ca7436ce114a7e38b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 19 May 2026 12:30:01 +0000
Subject: [PATCH] =?UTF-8?q?feat:=20add=20Lidskii=E2=80=93Last=20eigenvalue?=
 =?UTF-8?q?-perturbation=20eval=20problem?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds the Lidskii-Last theorem (§99 of Knill's "Some Fundamental
Theorems in Mathematics") as a new eval problem: for self-adjoint
complex matrices A, B with eigenvalues sorted in the same order, the
total eigenvalue displacement is bounded by the entrywise ℓ¹ distance.
Mathlib has no Lidskii, Ky Fan, or Hoffman-Wielandt perturbation bounds.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 LeanEval/LinearAlgebra/Lidskii.lean | 37 +++++++++++++++++++++++++++++
 manifests/problems.toml             | 11 +++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 LeanEval/LinearAlgebra/Lidskii.lean

diff --git a/LeanEval/LinearAlgebra/Lidskii.lean b/LeanEval/LinearAlgebra/Lidskii.lean
new file mode 100644
index 0000000..de73b6e
--- /dev/null
+++ b/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
diff --git a/manifests/problems.toml b/manifests/problems.toml
index b9e42d1..7f8cf35 100644
--- a/manifests/problems.toml
+++ b/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."