[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
cases isEmpty_or_nonempty n
[GOAL]
case inl
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : IsEmpty n
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
exfalso
[GOAL]
case inl.h
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : IsEmpty n
⊢ False
[PROOFSTEP]
exact hμ (Submodule.eq_bot_of_subsingleton _)
[GOAL]
case inr
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
obtain ⟨v, h_eg, h_nz⟩ := hμ.exists_hasEigenvector
[GOAL]
case inr.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz : v ≠ 0
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
obtain ⟨i, -, h_i⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty (fun i => ‖v i‖)
[GOAL]
case inr.intro.intro.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
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
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
⊢ v i ≠ 0
[PROOFSTEP]
contrapose! h_nz
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i = 0
⊢ v = 0
[PROOFSTEP]
ext j
[GOAL]
case h
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ v j = OfNat.ofNat 0 j
[PROOFSTEP]
rw [Pi.zero_apply, ← norm_le_zero_iff]
[GOAL]
case h
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ ‖v j‖ ≤ 0
[PROOFSTEP]
refine (h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)).trans ?_
[GOAL]
case h
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ ‖v i‖ ≤ 0
[PROOFSTEP]
exact norm_le_zero_iff.mpr h_nz
[GOAL]
case inr.intro.intro.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
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)
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
j : n
⊢ ‖v j * (v i)⁻¹‖ ≤ 1
[PROOFSTEP]
rw [norm_mul, norm_inv, mul_inv_le_iff' (norm_pos_iff.mpr h_nz), one_mul]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
j : n
⊢ ‖v j‖ ≤ ‖v i‖
[PROOFSTEP]
exact h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)
[GOAL]
case inr.intro.intro.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
simp_rw [mem_closedBall_iff_norm']
[GOAL]
case inr.intro.intro.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ∃ k, ‖A k k - μ‖ ≤ ∑ j in Finset.erase Finset.univ k, ‖A k j‖
[PROOFSTEP]
refine ⟨i, ?_⟩
[GOAL]
case inr.intro.intro.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖A i i - μ‖ ≤ ∑ j in Finset.erase Finset.univ i, ‖A i j‖
[PROOFSTEP]
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))
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖A i i - μ‖ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖
[PROOFSTEP]
congr
[GOAL]
case e_a
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ A i i - μ = (A i i * v i - μ * v i) * (v i)⁻¹
[PROOFSTEP]
field_simp [h_nz]
[GOAL]
case e_a
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ (A i i - μ) * v i = A i i * v i - μ * v i
[PROOFSTEP]
ring
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ = ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖
[PROOFSTEP]
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]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ μ * v i = ∑ x : n, A i x * v x
[PROOFSTEP]
rw [← Matrix.dotProduct, ← Matrix.mulVec]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ μ * v i = Matrix.mulVec A (fun x => v x) i
[PROOFSTEP]
exact (congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖ = ‖(∑ j in Finset.erase Finset.univ i, A i j * v j) * (v i)⁻¹‖
[PROOFSTEP]
rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖(∑ j in Finset.erase Finset.univ i, A i j * v j) * (v i)⁻¹‖ ≤
    ∑ j in Finset.erase Finset.univ i, ‖A i j‖ * ‖v j * (v i)⁻¹‖
[PROOFSTEP]
rw [Finset.sum_mul]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖∑ x in Finset.erase Finset.univ i, A i x * v x * (v i)⁻¹‖ ≤
    ∑ j in Finset.erase Finset.univ i, ‖A i j‖ * ‖v j * (v i)⁻¹‖
[PROOFSTEP]
exact (norm_sum_le _ _).trans (le_of_eq (by simp_rw [mul_assoc, norm_mul]))
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (↑Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ Module.End.eigenspace (↑Matrix.toLin' A) μ
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ∑ i_1 in Finset.erase Finset.univ i, ‖A i i_1 * v i_1 * (v i)⁻¹‖ =
    ∑ j in Finset.erase Finset.univ i, ‖A i j‖ * ‖v j * (v i)⁻¹‖
[PROOFSTEP]
simp_rw [mul_assoc, norm_mul]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ j in Finset.erase Finset.univ k, ‖A k j‖ < ‖A k k‖
⊢ Matrix.det A ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : Matrix.det A = 0
⊢ ∃ k, ‖A k k‖ ≤ ∑ j in Finset.erase Finset.univ k, ‖A k j‖
[PROOFSTEP]
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 )
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : Matrix.det A = 0
this : ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
⊢ ∃ k, ‖A k k‖ ≤ ∑ j in Finset.erase Finset.univ k, ‖A k j‖
[PROOFSTEP]
exact this.imp (fun a h ↦ by rwa [mem_closedBall_iff_norm', sub_zero] at h )
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h✝ : Matrix.det A = 0
this : ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
a : n
h : 0 ∈ Metric.closedBall (A a a) (∑ j in Finset.erase Finset.univ a, ‖A a j‖)
⊢ ‖A a a‖ ≤ ∑ j in Finset.erase Finset.univ a, ‖A a j‖
[PROOFSTEP]
rwa [mem_closedBall_iff_norm', sub_zero] at h 
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : Matrix.det A = 0
⊢ ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j in Finset.erase Finset.univ k, ‖A k j‖)
[PROOFSTEP]
refine eigenvalue_mem_ball ?_
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : Matrix.det A = 0
⊢ Module.End.HasEigenvalue (↑Matrix.toLin' fun k => A k) 0
[PROOFSTEP]
rw [Module.End.HasEigenvalue, Module.End.eigenspace_zero, ne_comm]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : Matrix.det A = 0
⊢ ⊥ ≠ LinearMap.ker (↑Matrix.toLin' fun k => A k)
[PROOFSTEP]
exact ne_of_lt (LinearMap.bot_lt_ker_of_det_eq_zero (by rwa [LinearMap.det_toLin']))
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : Matrix.det A = 0
⊢ ↑LinearMap.det (↑Matrix.toLin' fun k => A k) = 0
[PROOFSTEP]
rwa [LinearMap.det_toLin']
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i in Finset.erase Finset.univ k, ‖A i k‖ < ‖A k k‖
⊢ Matrix.det A ≠ 0
[PROOFSTEP]
rw [← Matrix.det_transpose]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i in Finset.erase Finset.univ k, ‖A i k‖ < ‖A k k‖
⊢ Matrix.det (Matrix.transpose A) ≠ 0
[PROOFSTEP]
exact det_ne_zero_of_sum_row_lt_diag (by simp_rw [Matrix.transpose_apply]; exact h)
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i in Finset.erase Finset.univ k, ‖A i k‖ < ‖A k k‖
⊢ ∀ (k : n), ∑ j in Finset.erase Finset.univ k, ‖Matrix.transpose A k j‖ < ‖Matrix.transpose A k k‖
[PROOFSTEP]
simp_rw [Matrix.transpose_apply]
[GOAL]
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i in Finset.erase Finset.univ k, ‖A i k‖ < ‖A k k‖
⊢ ∀ (k : n), ∑ x in Finset.erase Finset.univ k, ‖A x k‖ < ‖A k k‖
[PROOFSTEP]
exact h
