Totally nonnegative matrices

This file defines totally nonnegative matrices and provides basic API for them.

Main definitions

• Matrix.IsTotallyNonneg: a matrix is totally nonnegative if all its finite minors have nonnegative determinant.

Main results

• Matrix.IsTotallyNonneg.submatrix: any submatrix (with strictly monotonic row/column indices) of a totally nonnegative matrix is totally nonnegative.
• Matrix.IsTotallyNonneg.nonneg: any entry of a totally nonnegative matrix is nonnegative.
• Matrix.IsTotallyNonneg.zero: the zero matrix is totally nonnegative.
• Matrix.IsTotallyNonneg.one: the identity matrix is totally nonnegative.
• Matrix.IsTotallyNonneg.diagonal: a diagonal matrix with nonnegative diagonal entries is totally nonnegative.
• Matrix.IsTotallyNonneg.smul: a nonnegative scalar multiple of a totally nonnegative matrix is totally nonnegative.
• Matrix.IsTotallyNonneg.transpose: the transpose of a totally nonnegative matrix is totally nonnegative.
• Matrix.IsTotallyNonneg.conjTranspose: the conjugate transpose of a totally nonnegative matrix is totally nonnegative.

def Matrix.IsTotallyNonneg {ι : Type u_1} {R : Type u_3} [PartialOrder ι] [CommRing R] [PartialOrder R] (M : Matrix ι ι R) : Prop

A matrix is totally nonnegative if all its finite minors have nonnegative determinant.

Equations

• M.IsTotallyNonneg = ∀ ⦃n : ℕ⦄ ⦃rows cols : Fin n → ι⦄, StrictMono rows → StrictMono cols → 0 ≤ (M.submatrix rows cols).det

theorem Matrix.IsTotallyNonneg.submatrix {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [PartialOrder ι] [PartialOrder κ] [CommRing R] [PartialOrder R] {M : Matrix ι ι R} {f g : κ → ι} (hM : M.IsTotallyNonneg) (hf : StrictMono f) (hg : StrictMono g) : (M.submatrix f g).IsTotallyNonneg

theorem Matrix.IsTotallyNonneg.nonneg {ι : Type u_1} {R : Type u_3} [PartialOrder ι] [CommRing R] [PartialOrder R] {M : Matrix ι ι R} (hM : M.IsTotallyNonneg) (i j : ι) : 0 ≤ M i j

theorem Matrix.IsTotallyNonneg.transpose {ι : Type u_1} {R : Type u_3} [PartialOrder ι] [CommRing R] [PartialOrder R] {M : Matrix ι ι R} (hM : M.IsTotallyNonneg) : M.transpose.IsTotallyNonneg

@[simp]

theorem Matrix.isTotallyNonneg_transpose_iff {ι : Type u_1} {R : Type u_3} [PartialOrder ι] [CommRing R] [PartialOrder R] {M : Matrix ι ι R} : M.transpose.IsTotallyNonneg ↔ M.IsTotallyNonneg

theorem Matrix.IsTotallyNonneg.conjTranspose {ι : Type u_1} {R : Type u_3} [PartialOrder ι] [CommRing R] [PartialOrder R] {M : Matrix ι ι R} [StarRing R] [StarOrderedRing R] (hM : M.IsTotallyNonneg) : M.conjTranspose.IsTotallyNonneg

@[simp]

theorem Matrix.isTotallyNonneg_conjTranspose_iff {ι : Type u_1} {R : Type u_3} [PartialOrder ι] [CommRing R] [PartialOrder R] {M : Matrix ι ι R} [StarRing R] [StarOrderedRing R] : M.conjTranspose.IsTotallyNonneg ↔ M.IsTotallyNonneg

@[simp]

theorem Matrix.IsTotallyNonneg.zero {ι : Type u_1} {R : Type u_3} [PartialOrder ι] [CommRing R] [PartialOrder R] [IsOrderedRing R] : IsTotallyNonneg 0

theorem Matrix.IsTotallyNonneg.diagonal {ι : Type u_1} {R : Type u_3} [PartialOrder ι] [CommRing R] [PartialOrder R] [IsOrderedRing R] [DecidableEq ι] {f : ι → R} (hf : 0 ≤ f) : (diagonal f).IsTotallyNonneg

A diagonal matrix with nonnegative diagonal entries is totally nonnegative.

@[simp]

theorem Matrix.isTotallyNonneg_diagonal_iff {ι : Type u_1} {R : Type u_3} [PartialOrder ι] [CommRing R] [PartialOrder R] [IsOrderedRing R] [DecidableEq ι] {f : ι → R} : (diagonal f).IsTotallyNonneg ↔ 0 ≤ f

@[simp]

theorem Matrix.IsTotallyNonneg.one {ι : Type u_1} {R : Type u_3} [PartialOrder ι] [CommRing R] [PartialOrder R] [IsOrderedRing R] [DecidableEq ι] : IsTotallyNonneg 1

theorem Matrix.IsTotallyNonneg.smul {ι : Type u_1} {R : Type u_3} [PartialOrder ι] [CommRing R] [PartialOrder R] [IsOrderedRing R] {M : Matrix ι ι R} (hM : M.IsTotallyNonneg) {c : R} (hc : 0 ≤ c) : (c • M).IsTotallyNonneg

theorem Matrix.isTotallyNonneg_smul_iff {ι : Type u_1} [PartialOrder ι] {R : Type u_4} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Matrix ι ι R} {c : R} (hc : 0 < c) : (c • M).IsTotallyNonneg ↔ M.IsTotallyNonneg