Theorems · Theorem · linear algebra

eigenvalue_mem_ball

• 1000+ list: Gershgorin circle theorem

∀ {K : Type u_1} {n : Type u_2} [inst : NormedField K] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n K}
  {μ : K},
  Module.End.HasEigenvalue (Matrix.toLin' A) μ → ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)

Gershgorin's circle theorem: for any eigenvalue μ of a square matrix A, there exists an index k such that μ lies in the closed ball of center the diagonal term A k k and of radius the sum of the norms ∑ j ≠ k, ‖A k j‖.

Defined in

Mathlib.LinearAlgebra.Matrix.Gershgorin

Cited by

1 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldFintypeDecidableEq