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.

Reference

• https://en.wikipedia.org/wiki/Gershgorin_circle_theorem

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‖) : A.det ≠ 0

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‖) : A.det ≠ 0

If A is a column strictly dominant diagonal matrix, then its determinant is nonzero.