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 #

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) :

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) :

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