Ky Fan eigenvalue inequality

DefinitionPrefix sum of a finite real sequence#✓fully proved

For real numbers \(\lambda_0, \dots, \lambda_{n-1}\) and a natural number \(k \le n\), the prefix sum of length \(k\) is \(\sum_{i < k} \lambda_i\), the sum of the first \(k\) entries. Applied to the eigenvalues of a Hermitian matrix, listed in decreasing order, it is the sum of the \(k\) largest ones.

noncomputable def eigPrefSum {n : ℕ} (eig : Fin n → ℝ) (k : ℕ)
    (hk : k ≤ n) : ℝ :=
  ∑ i ∈ Finset.range k, if hi : i < k then eig (Fin.castLE hk ⟨i, hi⟩) else 0

Used by 1

Used byKy Fan inequality for sums of largest eigenvalues

TheoremKy Fan inequality for sums of largest eigenvalues#✓fully proved

Let \(A\) and \(B\) be Hermitian \(n \times n\) complex matrices and let \(k \le n\). Then the sum of the \(k\) largest eigenvalues of \(A + B\) is at most the sum of the \(k\) largest eigenvalues of \(A\) plus the sum of the \(k\) largest eigenvalues of \(B\), where eigenvalues are counted with multiplicity.

theorem ky_fan_eigenvalue_sum_le
    {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℂ)
    (hA : A.IsHermitian) (hB : B.IsHermitian)
    (k : ℕ) (hk : k ≤ n) :
    let hA_sym := (Matrix.isSymmetric_toEuclideanLin_iff.mpr hA)
    let hB_sym := (Matrix.isSymmetric_toEuclideanLin_iff.mpr hB)
    let hAB_sym := (Matrix.isSymmetric_toEuclideanLin_iff.mpr (hA.add hB))
    eigPrefSum (hAB_sym.eigenvalues finrank_euclideanSpace_fin) k hk ≤
      eigPrefSum (hA_sym.eigenvalues finrank_euclideanSpace_fin) k hk +
        eigPrefSum (hB_sym.eigenvalues finrank_euclideanSpace_fin) k hk

Sources

• Ky Fan, On a theorem of Weyl, PNAS 35 (1949), 652-655, DOI 10.1073/pnas.35.11.652.

Uses 1

Statement usesPrefix sum of a finite real sequence

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.