Gershgorin's circle theorem #
This file gives the proof of Gershgorin's circle theorem eigenvalue_mem_ball on the eigenvalues
of matrices and some applications.
References #
theorem eigenvalue_mem_ball {K : Type u_1} {n : Type u_2} [NormedField K] [Fintype n] [DecidableEq n] {A : Matrix n n K} {μ : K} (hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ) :
∃ (k : n), μ ∈ 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‖.
theorem det_ne_zero_of_sum_row_lt_diag {K : Type u_1} {n : Type u_2} [NormedField K] [Fintype n] [DecidableEq n] {A : Matrix n n K} (h : ∀ (k : n), ∑ j ∈ Finset.univ.erase k, ‖A k j‖ < ‖A k k‖) :
If A is a row strictly dominant diagonal matrix, then its determinant is nonzero.
theorem det_ne_zero_of_sum_col_lt_diag {K : Type u_1} {n : Type u_2} [NormedField K] [Fintype n] [DecidableEq n] {A : Matrix n n K} (h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖) :
If A is a column strictly dominant diagonal matrix, then its determinant is nonzero.