feat: proof of Gershgorin's circle theorem and some applications (#6436)

Prove [Gershgorin circle theorem](https://en.wikipedia.org/wiki/Gershgorin_circle_theorem) and some applications that will be useful for the proof of Dirichlet's unit theorem #5960

Mathlib.lean

@@ -2218,6 +2218,7 @@ import Mathlib.LinearAlgebra.Matrix.DotProduct
 import Mathlib.LinearAlgebra.Matrix.Dual
 import Mathlib.LinearAlgebra.Matrix.FiniteDimensional
 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup
+import Mathlib.LinearAlgebra.Matrix.Gershgorin
 import Mathlib.LinearAlgebra.Matrix.Hermitian
 import Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
 import Mathlib.LinearAlgebra.Matrix.IsDiag

Mathlib/LinearAlgebra/Matrix/Gershgorin.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2023 Xavier Roblot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Xavier Roblot
+-/
+import Mathlib.Analysis.Normed.Field.Basic
+import Mathlib.LinearAlgebra.Eigenspace.Basic
+import Mathlib.LinearAlgebra.Determinant
+
+/-!
+# 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
+-/
+
+open BigOperators
+
+variable {K n : Type*} [NormedField K] [Fintype n] [DecidableEq n] {A : Matrix n n K}
+
+/-- **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 eigenvalue_mem_ball {μ : K} (hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ) :
+      ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.univ.erase k, ‖A k j‖) := by
+  cases isEmpty_or_nonempty n
+  · exfalso
+    exact hμ (Submodule.eq_bot_of_subsingleton _)
+  · obtain ⟨v, h_eg, h_nz⟩ := hμ.exists_hasEigenvector
+    obtain ⟨i, -, h_i⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty (fun i => ‖v i‖)
+    have h_nz : v i ≠ 0 := by
+      contrapose! h_nz
+      ext j
+      rw [Pi.zero_apply, ← norm_le_zero_iff]
+      refine (h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)).trans ?_
+      exact norm_le_zero_iff.mpr h_nz
+    have h_le : ∀ j, ‖v j * (v i)⁻¹‖ ≤ 1 := fun j => by
+      rw [norm_mul, norm_inv, mul_inv_le_iff' (norm_pos_iff.mpr h_nz), one_mul]
+      exact h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)
+    simp_rw [mem_closedBall_iff_norm']
+    refine ⟨i, ?_⟩
+    calc
+      _ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ := by congr; field_simp [h_nz]; ring
+      _ = ‖(A i i * v i - ∑ j, A i j * v j) * (v i)⁻¹‖ := by
+                rw [show μ * v i = ∑ x : n, A i x * v x by
+                  rw [← Matrix.dotProduct, ← Matrix.mulVec]
+                  exact (congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm]
+      _ = ‖(∑ j in Finset.univ.erase i, A i j * v j) * (v i)⁻¹‖ := by
+                rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
+      _ ≤ ∑ j in Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖ := by
+                rw [Finset.sum_mul]
+                exact (norm_sum_le _ _).trans (le_of_eq (by simp_rw [mul_assoc, norm_mul]))
+      _ ≤ ∑ j in Finset.univ.erase i, ‖A i j‖ :=
+                (Finset.sum_le_sum fun j _ => mul_le_of_le_one_right (norm_nonneg _) (h_le j))
+
+/-- If `A` is a row strictly dominant diagonal matrix, then it's determinant is nonzero. -/
+theorem det_ne_zero_of_sum_row_lt_diag (h : ∀ k, ∑ j in Finset.univ.erase k, ‖A k j‖ < ‖A k k‖) :
+    A.det ≠ 0 := by
+  contrapose! h
+  suffices ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j in Finset.univ.erase k, ‖A k j‖) by
+    exact this.imp (fun a h ↦ by rwa [mem_closedBall_iff_norm', sub_zero] at h)
+  refine eigenvalue_mem_ball ?_
+  rw [Module.End.HasEigenvalue,  Module.End.eigenspace_zero, ne_comm]
+  exact ne_of_lt (LinearMap.bot_lt_ker_of_det_eq_zero (by rwa [LinearMap.det_toLin']))
+
+/-- If `A` is a column strictly dominant diagonal matrix, then it's determinant is nonzero. -/
+theorem det_ne_zero_of_sum_col_lt_diag (h : ∀ k, ∑ i in Finset.univ.erase k, ‖A i k‖ < ‖A k k‖) :
+    A.det ≠ 0 := by
+  rw [← Matrix.det_transpose]
+  exact det_ne_zero_of_sum_row_lt_diag (by simp_rw [Matrix.transpose_apply]; exact h)

Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean

@@ -33,15 +33,16 @@ matrix, linear_equiv, determinant, inverse
 
 -/
 
+variable {n : Type*} [Fintype n]
 
 namespace Matrix
 
+section LinearEquiv
+
 open LinearMap
 
 variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
 
-variable {n : Type*} [Fintype n]
-
 section ToLinearEquiv'
 
 variable [DecidableEq n]
@@ -196,4 +197,52 @@ alias nondegenerate_iff_det_ne_zero ↔ Nondegenerate.det_ne_zero Nondegenerate.
 
 end Nondegenerate
 
+end LinearEquiv
+
+section Determinant
+
+open BigOperators
+
+/-- A matrix whose nondiagonal entries are negative with the sum of the entries of each
+column positive has nonzero determinant. -/
+lemma det_ne_zero_of_sum_col_pos [DecidableEq n] {S : Type*} [LinearOrderedCommRing S]
+    {A : Matrix n n S} (h1 : ∀ i j, i ≠ j → A i j < 0) (h2 : ∀ j, 0 < ∑ i, A i j) :
+    A.det ≠ 0 := by
+  cases isEmpty_or_nonempty n
+  · simp
+  · contrapose! h2
+    obtain ⟨v, ⟨h_vnz, h_vA⟩⟩ := Matrix.exists_vecMul_eq_zero_iff.mpr h2
+    wlog h_sup : 0 < Finset.sup' Finset.univ Finset.univ_nonempty v
+    · refine this h1 inferInstance h2 (-1 • v) ?_ ?_ ?_
+      · exact smul_ne_zero (by norm_num) h_vnz
+      · rw [Matrix.vecMul_smul, h_vA, smul_zero]
+      · obtain ⟨i, hi⟩ := Function.ne_iff.mp h_vnz
+        simp_rw [Finset.lt_sup'_iff, Finset.mem_univ, true_and] at h_sup ⊢
+        simp_rw [not_exists, not_lt] at h_sup
+        refine ⟨i, ?_⟩
+        rw [Pi.smul_apply, neg_smul, one_smul, Left.neg_pos_iff]
+        refine Ne.lt_of_le hi (h_sup i)
+    · obtain ⟨j₀, -, h_j₀⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty v
+      refine ⟨j₀, ?_⟩
+      rw [← mul_le_mul_left (h_j₀ ▸ h_sup), Finset.mul_sum, mul_zero]
+      rw [show 0 = ∑ i, v i * A i j₀ from (congrFun h_vA j₀).symm]
+      refine Finset.sum_le_sum (fun i hi => ?_)
+      by_cases h : i = j₀
+      · rw [h]
+      · exact (mul_le_mul_right_of_neg (h1 i j₀ h)).mpr (h_j₀ ▸ Finset.le_sup' v hi)
+
+/-- A matrix whose nondiagonal entries are negative with the sum of the entries of each
+row positive has nonzero determinant. -/
+lemma det_ne_zero_of_sum_row_pos [DecidableEq n] {S : Type*} [LinearOrderedCommRing S]
+    {A : Matrix n n S} (h1 : ∀ i j, i ≠ j → A i j < 0) (h2 : ∀ i, 0 < ∑ j, A i j) :
+    A.det ≠ 0 := by
+  rw [← Matrix.det_transpose]
+  refine det_ne_zero_of_sum_col_pos ?_ ?_
+  · simp_rw [Matrix.transpose_apply]
+    exact fun i j h => h1 j i h.symm
+  · simp_rw [Matrix.transpose_apply]
+    exact h2
+
+end Determinant
+
 end Matrix