# Documentation

Mathlib.LinearAlgebra.Matrix.Gershgorin

# 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} [] [] [] {A : Matrix n n K} {μ : K} (hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ) :
k, μ Metric.closedBall (A k k) (Finset.sum (Finset.erase Finset.univ k) fun j => 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} [] [] [] {A : Matrix n n K} (h : ∀ (k : n), (Finset.sum (Finset.erase Finset.univ k) fun j => A k j) < A k k) :
0

If A is a row strictly dominant diagonal matrix, then it's determinant is nonzero.

theorem det_ne_zero_of_sum_col_lt_diag {K : Type u_1} {n : Type u_2} [] [] [] {A : Matrix n n K} (h : ∀ (k : n), (Finset.sum (Finset.erase Finset.univ k) fun i => A i k) < A k k) :
0

If A` is a column strictly dominant diagonal matrix, then it's determinant is nonzero.