Lidskii's inequality

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).

theorem declaration uses `sorry`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 := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℂB:Matrix n n ℂhA:A.IsHermitianhB:B.IsHermitianp:ℝ_hp:1 ≤ p⊢ ∑ j, |hA.eigenvalues₀ j - hB.eigenvalues₀ j| ^ p ≤ ∑ j, |⋯.eigenvalues₀ j| ^ p
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on May 29, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 31, 2026