From 2fd2fffa968823755090ab38c1fbab96011469f5 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 May 2026 23:46:25 +0000
Subject: [PATCH] feat: add Lidskii's inequality eval problem
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds Lidskii's inequality (§99 of Knill's "Some Fundamental
Theorems in Mathematics", an additional statement of the section; the
boxed main theorem `lidskii_last` is the p = 1 case combined with an
entrywise bound) as a new eval problem: for self-adjoint complex
matrices A, B with eigenvalues sorted in the same order and p ≥ 1,
∑_j |α_j - β_j|^p ≤ ∑_j |γ_j|^p where γ_j are the eigenvalues of B - A.
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/LidskiiInequality.lean | 42 +++++++++++++++++++
 manifests/problems.toml                       | 11 +++++
 2 files changed, 53 insertions(+)
 create mode 100644 LeanEval/LinearAlgebra/LidskiiInequality.lean

diff --git a/LeanEval/LinearAlgebra/LidskiiInequality.lean b/LeanEval/LinearAlgebra/LidskiiInequality.lean
new file mode 100644
index 0000000..585fe77
--- /dev/null
+++ b/LeanEval/LinearAlgebra/LidskiiInequality.lean
@@ -0,0 +1,42 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace LinearAlgebra
+
+/-!
+# Lidskii's inequality
+
+§99 of Oliver Knill's *Some Fundamental Theorems in Mathematics* (an
+additional statement of the section on spectral perturbation; the boxed
+main theorem `lidskii_last` follows as the `p = 1` case combined with an
+entrywise bound).
+
+For two self-adjoint complex `n × n` matrices `A, B` with eigenvalues
+sorted in the same order, the `ℓ^p` displacement of the eigenvalues is
+bounded by the `ℓ^p` norm of the eigenvalues of `C := B − A`, for every
+real `p ≥ 1`:
+
+  `∑ⱼ |αⱼ − βⱼ|^p ≤ ∑ⱼ |γⱼ|^p`.
+
+mathlib has `Matrix.IsHermitian.eigenvalues₀` (the spectral-theorem
+eigenvalues) but none of the classical eigenvalue-perturbation bounds
+(Lidskii, Ky Fan, Hoffman–Wielandt). No formalization of Lidskii's
+inequality was found in any other proof assistant.
+-/
+
+open Matrix
+
+/-- **Lidskii's inequality.** For two self-adjoint complex `n × n` matrices
+`A, B`, with eigenvalues sorted in the same order and `p ≥ 1`,
+`∑ⱼ |αⱼ − βⱼ|^p ≤ ∑ⱼ |γⱼ|^p` where `γⱼ` are the eigenvalues of `B − A`. -/
+@[eval_problem]
+theorem lidskii_inequality {n : Type*} [Fintype n] [DecidableEq n]
+    {A B : Matrix n n ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian)
+    {p : ℝ} (_hp : 1 ≤ p) :
+    ∑ j, |hA.eigenvalues₀ j - hB.eigenvalues₀ j| ^ p ≤
+      ∑ j, |(hB.sub hA).eigenvalues₀ j| ^ p := by
+  sorry
+
+end LinearAlgebra
+end LeanEval
diff --git a/manifests/problems.toml b/manifests/problems.toml
index b9e42d1..c2e2a35 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_inequality"
+title = "Lidskii's inequality"
+test = false
+module = "LeanEval.LinearAlgebra.LidskiiInequality"
+holes = ["lidskii_inequality"]
+submitter = "Kim Morrison"
+notes = "§99 of Oliver Knill's 'Some Fundamental Theorems in Mathematics' (additional statement of the section on spectral perturbation; the boxed main theorem lidskii_last is the p = 1 case combined with an entrywise bound). For self-adjoint complex matrices A, B with eigenvalues sorted in the same order and p ≥ 1, ∑_j |α_j - β_j|^p ≤ ∑_j |γ_j|^p where γ_j are the eigenvalues of B - A. Uses Matrix.IsHermitian.eigenvalues₀; mathlib has no Lidskii, Ky Fan, or Hoffman-Wielandt perturbation bounds, and no formalization of Lidskii's inequality was found in any other proof assistant. Companion problem: lidskii_last (#274) is the p = 1 entrywise-distance corollary."
+source = "V. B. Lidskii, On the proper values of a sum and product of symmetric matrices, Dokl. Akad. Nauk SSSR 75 (1950), 769-772. Listed as an additional statement of §99 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf)."
+informal_solution = "The eigenvalues of B = A + C interlace those of A according to Weyl's inequalities, giving componentwise α_j + γ_n ≤ β_j ≤ α_j + γ_1 for sorted eigenvalues; tightening this via the Ky Fan extremal characterization of partial sums of eigenvalues (∑_{j=1}^k α_j = max{tr(P A) : P projection of rank k}) yields the majorization ∑_{j=1}^k (β_j - α_j)_↓ ≤ ∑_{j=1}^k γ_j for sorted differences. Schur's theorem on Hermitian matrices then upgrades the partial-sum majorization to ∑_j |α_j - β_j|^p ≤ ∑_j |γ_j|^p for any convex function applied componentwise, in particular x ↦ |x|^p for p ≥ 1 (Hardy-Littlewood-Pólya / Hardy-Littlewood majorization principle)."