det_ne_zero_of_sum_row_lt_diag
theorem det_ne_zero_of_sum_row_lt_diag :
∀ {K : Type u_1} {n : Type u_2} [inst : NormedField K] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
{A : Matrix n n K}, (∀ (k : n), ((Finset.univ.erase k).sum fun j => ‖A k j‖) < ‖A k k‖) → A.det ≠ 0
This theorem states that if we have a matrix `A` with elements from a normed field `K` and indices from a finite type `n`, then if `A` is a row strictly dominant diagonal matrix (i.e., for each row, the norm of the diagonal element is strictly greater than the sum of norms of all other elements in the row), then the determinant of `A` is not equal to 0. The equality comparison for the type `n` is assumed to be decidable.
More concisely: If `A` is an `n x n` matrix over a normed field with row-strictly dominant diagonals, then the determinant of `A` is nonzero.
|
det_ne_zero_of_sum_col_lt_diag
theorem det_ne_zero_of_sum_col_lt_diag :
∀ {K : Type u_1} {n : Type u_2} [inst : NormedField K] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
{A : Matrix n n K}, (∀ (k : n), ((Finset.univ.erase k).sum fun i => ‖A i k‖) < ‖A k k‖) → A.det ≠ 0
The theorem `det_ne_zero_of_sum_col_lt_diag` states that: given a column strictly dominant diagonal matrix `A` with entries in a normed field `K` and indexed over a type `n`, which has decidable equality and is finitely enumerable, if for every column index `k`, the sum of norms of entries in column `k` excluding the diagonal entry `A k k` is strictly less than the norm of `A k k`, then the determinant of `A` is not zero.
More concisely: If `A` is a column strictly dominant diagonal matrix over a normed field `K` with decidable equality and finite index type `n`, then the determinant of `A` is non-zero if and only if the sum of the norms of off-diagonal entries in each column is strictly less than the norm of the corresponding diagonal entry.
|
eigenvalue_mem_ball
theorem eigenvalue_mem_ball :
∀ {K : Type u_1} {n : Type u_2} [inst : NormedField K] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
{A : Matrix n n K} {μ : K},
Module.End.HasEigenvalue (Matrix.toLin' A) μ →
∃ k, μ ∈ Metric.closedBall (A k k) ((Finset.univ.erase k).sum fun j => ‖A k j‖)
**Gershgorin's circle theorem**: This theorem states that for any given eigenvalue `μ` of a square matrix `A` of a normed field `K`, there exists an index `k` such that the eigenvalue `μ` lies within the closed ball centered at the diagonal term `A k k` of the matrix and with a radius equal to the sum of the norms of terms `A k j`, for all `j` not equal to `k`. This closed ball is within a metric space defined by the distance function of the field `K`. The theorem applies to all types `K` that form a normed field and any type `n` that has finite elements and a defined equality function.
More concisely: For any square matrix over a normed field, each eigenvalue lies in the closed disk centered at the corresponding diagonal entry with radius equal to the sum of the norms of entries in other columns.
|