Weyl's eigenvalue inequalities

TheoremWeyl's inequality (upper bound)#✓fully proved

For self-adjoint operators T, S, λ_{a+b}(T + S) ≤ λ_a(T) + λ_b(S) whenever a + b < n.

theorem weyl_eigenvalue_add_le {n : ℕ} {T S : E →ₗ[𝕜] E}
    (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
    {a b : ℕ} (ha : a < n) (hb : b < n) (hab : a + b < n) :
    (hT.add hS).eigenvalues hn ⟨a + b, hab⟩ ≤
      hT.eigenvalues hn ⟨a, ha⟩ + hS.eigenvalues hn ⟨b, hb⟩

Uses 7 · Used by 1

Proof usesDimension of the span of the eigenbasis head · Dimension of the span of the eigenbasis tail · Head of an orthonormal eigenbasis · Rayleigh form of an operator · Lower bound for the Rayleigh form on the eigenbasis head · Upper bound for the Rayleigh form on the eigenbasis tail · Tail of an orthonormal eigenbasis

Used byWeyl's inequality (upper bound), matrix form

TheoremWeyl's inequality (lower bound)#✓fully proved

For self-adjoint operators T, S, λ_a(T) + λ_b(S) ≤ λ_{a+b-(n-1)}(T + S) whenever n - 1 ≤ a + b.

theorem le_weyl_eigenvalue_add {n : ℕ} {T S : E →ₗ[𝕜] E}
    (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
    {a b : ℕ} (ha : a < n) (hb : b < n) (hab : n - 1 ≤ a + b) :
    hT.eigenvalues hn ⟨a, ha⟩ + hS.eigenvalues hn ⟨b, hb⟩ ≤
      (hT.add hS).eigenvalues hn ⟨a + b - (n - 1), by omega⟩

Uses 7 · Used by 1

Proof usesDimension of the span of the eigenbasis head · Dimension of the span of the eigenbasis tail · Head of an orthonormal eigenbasis · Rayleigh form of an operator · Lower bound for the Rayleigh form on the eigenbasis head · Upper bound for the Rayleigh form on the eigenbasis tail · Tail of an orthonormal eigenbasis

Used byWeyl's inequality (lower bound), matrix form

TheoremWeyl's inequality (upper bound), matrix form#✓fully proved

For Hermitian matrices A, B, λ_{a+b}(A + B) ≤ λ_a(A) + λ_b(B) whenever a + b < n.

theorem _root_.Matrix.IsHermitian.eigenvalues₀_add_le {n : ℕ}
    {A B : Matrix (Fin n) (Fin n) 𝕜}
    (hA : A.IsHermitian) (hB : B.IsHermitian)
    {a b : ℕ} (ha : a < n) (hb : b < n) (hab : a + b < n) :
    _root_.Matrix.IsHermitian.eigenvalues₀ (_root_.Matrix.IsHermitian.add hA hB)
        ⟨a + b, by simpa using hab⟩ ≤
      _root_.Matrix.IsHermitian.eigenvalues₀ hA ⟨a, by simpa using ha⟩ +
        _root_.Matrix.IsHermitian.eigenvalues₀ hB ⟨b, by simpa using hb⟩

Uses 1

Proof usesWeyl's inequality (upper bound)

TheoremWeyl's inequality (lower bound), matrix form#✓fully proved

For Hermitian matrices A, B, λ_a(A) + λ_b(B) ≤ λ_{a+b-(n-1)}(A + B) whenever n - 1 ≤ a + b.

theorem _root_.Matrix.IsHermitian.le_eigenvalues₀_add {n : ℕ}
    {A B : Matrix (Fin n) (Fin n) 𝕜}
    (hA : A.IsHermitian) (hB : B.IsHermitian)
    {a b : ℕ} (ha : a < n) (hb : b < n) (hab : n - 1 ≤ a + b) :
    _root_.Matrix.IsHermitian.eigenvalues₀ hA ⟨a, by simpa using ha⟩ +
        _root_.Matrix.IsHermitian.eigenvalues₀ hB ⟨b, by simpa using hb⟩ ≤
      _root_.Matrix.IsHermitian.eigenvalues₀ (_root_.Matrix.IsHermitian.add hA hB)
        ⟨a + b - (n - 1), by simpa using (by omega : a + b - (n - 1) < n)⟩

Uses 1

Proof usesWeyl's inequality (lower bound)

TheoremEigenvalues of equal Hermitian matrices agree#✓fully proved

Eigenvalues are unchanged when the matrix is replaced by an equal matrix (useful to transport eigenvalue computations along identities such as diagonal d₁ + diagonal d₂ = diagonal (d₁ + d₂)).

theorem _root_.Matrix.IsHermitian.eigenvalues₀_congr {n : ℕ}
    {A B : Matrix (Fin n) (Fin n) 𝕜}
    (h : A = B) (hA : A.IsHermitian) (hB : B.IsHermitian) :
    _root_.Matrix.IsHermitian.eigenvalues₀ hA = _root_.Matrix.IsHermitian.eigenvalues₀ hB

TheoremEigenvalues of a diagonal matrix with decreasing entries#✓fully proved

The eigenvalues of a diagonal Hermitian matrix whose diagonal entries are already in decreasing order are exactly those entries.

theorem _root_.Matrix.IsHermitian.eigenvalues₀_diagonal_of_antitone {n : ℕ}
    {d : Fin n → ℝ} (hd : Antitone d) (i : Fin (Fintype.card (Fin n))) :
    _root_.Matrix.IsHermitian.eigenvalues₀
        (Matrix.isHermitian_diagonal_of_self_adjoint (fun i => (d i : 𝕜))
          (by
            funext j
            rw [Pi.star_apply, RCLike.star_def]
            exact RCLike.conj_ofReal _)) i =
      d ⟨i.val, by simpa using i.isLt⟩

TheoremWeyl's perturbation inequality#✓fully proved

Let \(A\) and \(B\) be Hermitian \(n \times n\) complex matrices, and let \(\lambda_1(A) \ge \dots \ge \lambda_n(A)\) and \(\lambda_1(B) \ge \dots \ge \lambda_n(B)\) be their eigenvalues, listed with multiplicity in decreasing order. Then \(|\lambda_i(A) - \lambda_i(B)| \le \|A - B\|\) for every \(i\), where \(\|A - B\|\) is the operator norm of \(A - B\) acting on \(\mathbb{C}^n\) with the Euclidean norm.

theorem weyl_eigenvalue_perturbation_le
    {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℂ)
    (hA : A.IsHermitian) (hB : B.IsHermitian) (i : Fin n) :
    let hA_sym := Matrix.isSymmetric_toEuclideanLin_iff.mpr hA
    let hB_sym := Matrix.isSymmetric_toEuclideanLin_iff.mpr hB

Sources

• H. Weyl, Math. Ann. 71 (1912), DOI 10.1007/BF01456804.

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.