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) (Finset.sum (Finset.erase Finset.univ k) fun (j : n) => ‖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), (Finset.sum (Finset.erase Finset.univ k) fun (j : n) => ‖A k j‖) < ‖A k k‖)
:
Matrix.det A ≠ 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}
[NormedField K]
[Fintype n]
[DecidableEq n]
{A : Matrix n n K}
(h : ∀ (k : n), (Finset.sum (Finset.erase Finset.univ k) fun (i : n) => ‖A i k‖) < ‖A k k‖)
:
Matrix.det A ≠ 0
If A is a column strictly dominant diagonal matrix, then it's determinant is nonzero.