Lidskii's eigenvalue inequality

TheoremLidskii's inequality#●ready to prove

Let \(A\) and \(B\) be Hermitian complex square matrices indexed by a finite set with \(N\) elements. List the eigenvalues of \(A\), of \(B\) and of \(B - A\), each with multiplicity and in decreasing order, as \(\alpha_1 \ge \dots \ge \alpha_N\), \(\beta_1 \ge \dots \ge \beta_N\) and \(\gamma_1 \ge \dots \ge \gamma_N\). Then for every real \(p \ge 1\),

\[\sum_{j=1}^N |\alpha_j - \beta_j|^p \le \sum_{j=1}^N |\gamma_j|^p.\]

public theorem_wanted 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

Sources

• 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). Problem lidskii_inequality of the lean-eval benchmark.

TheoremLidskii–Last theorem#●ready to prove

Let \(A\) and \(B\) be Hermitian complex square matrices indexed by a finite set with \(N\) elements, and list the eigenvalues of \(A\) and of \(B\), each with multiplicity and in decreasing order, as \(\alpha_1 \ge \dots \ge \alpha_N\) and \(\beta_1 \ge \dots \ge \beta_N\). Then

\[\sum_{j=1}^N |\alpha_j - \beta_j| \le \sum_{i,j} |A_{ij} - B_{ij}|.\]

public theorem_wanted 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‖

Sources

• 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). Problem lidskii_last of the lean-eval benchmark.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.