Documentation

Mathlib.LinearAlgebra.Matrix.Determinant.TotallyNonneg

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.

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

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

Instances For

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

@[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