English
If all off-diagonal entries are negative and each row sums to a positive number, then det is nonzero.
Русский
Если все элементы вне диагонали отрицательны, а сумма по каждой строке положительна, детерминант не равен нулю.
LaTeX
$$$\\det A \\neq 0 \\quad\\text{if off\\-diagonal entries negative and row sums positive}$$$
Lean4
/-- A matrix whose nondiagonal entries are negative with the sum of the entries of each
column positive has nonzero determinant. -/
theorem det_ne_zero_of_sum_col_pos [DecidableEq n] {S : Type*} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S]
{A : Matrix n n S} (h1 : Pairwise fun 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) (by simp [*]) ?_ ?_
· rw [Matrix.smul_vecMul, 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]
exact 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_iff_right₀ (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 h)).mpr (h_j₀ ▸ Finset.le_sup' v hi)
