Total nonnegativity

A real matrix is totally nonnegative when every square minor formed by strictly increasing index maps is nonnegative. The empty (k = 0) minor is the determinant of a Matrix (Fin 0) (Fin 0), which Mathlib sets to 1.

Cauchy–Binet is proved only for a product with middle dimension 3, by enumerating the C(3, r) strictly increasing maps Fin r → Fin 3 (r = 0,1,2,3) and using rank for r > 3.

TN01: definition

def BollobasNikiforov.IsTotallyNonneg {m : Type u_1} {n : Type u_2} [LinearOrder m] [LinearOrder n] (A : Matrix m n ℝ) : Prop

A matrix is totally nonnegative if every square minor with strictly increasing row and column index maps has nonnegative determinant. The k = 0 case is included: Matrix.det_fin_zero says the empty minor equals 1.

Equations

• BollobasNikiforov.IsTotallyNonneg A = ∀ (k : ℕ) (I : Fin k → m) (J : Fin k → n), StrictMono I → StrictMono J → 0 ≤ (A.submatrix I J).det

TN02: size-one minors and nondecreasing index maps

theorem BollobasNikiforov.strictMono_of_monotone_injective {α : Type u_3} {β : Type u_4} [LinearOrder α] [PartialOrder β] {f : α → β} (hmono : Monotone f) (hinj : Function.Injective f) : StrictMono f

A monotone injective map out of a linear order is strictly increasing.

theorem BollobasNikiforov.IsTotallyNonneg.apply {m : Type u_1} {n : Type u_2} [LinearOrder m] [LinearOrder n] {A : Matrix m n ℝ} (hA : IsTotallyNonneg A) (i : m) (j : n) : 0 ≤ A i j

Totally nonnegative matrices are entrywise nonnegative (the k = 1 minors).

theorem BollobasNikiforov.det_submatrix_eq_zero_of_not_injective {m : Type u_1} {n : Type u_2} {k : ℕ} (A : Matrix m n ℝ) {I : Fin k → m} {J : Fin k → n} (h : ¬Function.Injective I ∨ ¬Function.Injective J) : (A.submatrix I J).det = 0

theorem BollobasNikiforov.IsTotallyNonneg.det_submatrix_monotone {m : Type u_1} {n : Type u_2} [LinearOrder m] [LinearOrder n] {A : Matrix m n ℝ} (hA : IsTotallyNonneg A) {k : ℕ} {I : Fin k → m} {J : Fin k → n} (hI : Monotone I) (hJ : Monotone J) : 0 ≤ (A.submatrix I J).det

If A is totally nonnegative and I, J are merely nondecreasing, the corresponding minor is still nonnegative: a repeated index forces determinant 0 when k ≥ 2, and an injective monotone map is strictly increasing.

TN03: Cauchy–Binet of width 3

@[reducible, inline]

abbrev BollobasNikiforov.StrictMonoFin3 (r : ℕ) : Type

Strictly increasing maps Fin r → Fin 3. There are C(3, r) of them for r ≤ 3, and none when r > 3.

Equations

• BollobasNikiforov.StrictMonoFin3 r = { f : Fin r → Fin 3 // StrictMono f }

@[instance_reducible]

instance BollobasNikiforov.decidablePredStrictMonoFin3 {r : ℕ} : DecidablePred fun (f : Fin r → Fin 3) => StrictMono f

Equations

• BollobasNikiforov.decidablePredStrictMonoFin3 = inferInstance

@[instance_reducible]

noncomputable instance BollobasNikiforov.instFintypeStrictMonoFin3 {r : ℕ} : Fintype (StrictMonoFin3 r)

Equations

• BollobasNikiforov.instFintypeStrictMonoFin3 = Subtype.fintype StrictMono

theorem BollobasNikiforov.det_eq_zero_of_rank_lt {r : ℕ} {A : Matrix (Fin r) (Fin r) ℝ} (h : A.rank < r) : A.det = 0

theorem BollobasNikiforov.det_mul_eq_zero_of_three_lt {r : ℕ} (hr : 3 < r) (P : Matrix (Fin r) (Fin 3) ℝ) (Q : Matrix (Fin 3) (Fin r) ℝ) : (P * Q).det = 0

theorem BollobasNikiforov.isEmpty_strictMonoFin3_of_three_lt {r : ℕ} (hr : 3 < r) : IsEmpty (StrictMonoFin3 r)

theorem BollobasNikiforov.strictMono_eq_id {k : ℕ} {f : Fin k → Fin k} (hf : StrictMono f) : f = id

theorem BollobasNikiforov.exists_eq_succAbove_of_strictMono {f : Fin 2 → Fin 3} (hf : StrictMono f) : ∃ (k : Fin 3), f = k.succAbove

def BollobasNikiforov.succAboveStrictMono (k : Fin 3) : StrictMonoFin3 2

The three strictly increasing maps Fin 2 → Fin 3 are Fin.succAbove k for k : Fin 3 (skip one of {0,1,2}).

Equations

• BollobasNikiforov.succAboveStrictMono k = ⟨k.succAbove, ⋯⟩

theorem BollobasNikiforov.succAboveStrictMono_bijective : Function.Bijective succAboveStrictMono

def BollobasNikiforov.constStrictMono (k : Fin 3) : StrictMonoFin3 1

All maps Fin 1 → Fin 3 are strictly monotone (the domain is a subsingleton).

Equations

• BollobasNikiforov.constStrictMono k = ⟨fun (x : Fin 1) => k, ⋯⟩

theorem BollobasNikiforov.constStrictMono_bijective : Function.Bijective constStrictMono

theorem BollobasNikiforov.det_mul_width3_two (P : Matrix (Fin 2) (Fin 3) ℝ) (Q : Matrix (Fin 3) (Fin 2) ℝ) : (P * Q).det = (P.submatrix id (Fin.succAbove 0)).det * (Q.submatrix (Fin.succAbove 0) id).det + (P.submatrix id (Fin.succAbove 1)).det * (Q.submatrix (Fin.succAbove 1) id).det + (P.submatrix id (Fin.succAbove 2)).det * (Q.submatrix (Fin.succAbove 2) id).det

Direct expansion of a 2 × 2 determinant of a product through width 3.

theorem BollobasNikiforov.det_mul_eq_sum_strictMono_width3 {r : ℕ} (P : Matrix (Fin r) (Fin 3) ℝ) (Q : Matrix (Fin 3) (Fin r) ℝ) : (P * Q).det = ∑ S : StrictMonoFin3 r, (P.submatrix id ↑S).det * (Q.submatrix (↑S) id).det

Cauchy–Binet for P * Q with middle index Fin 3.

theorem BollobasNikiforov.submatrix_mul_transpose {ι : Type u_3} {κ : Type u_4} {r : ℕ} (X : Matrix ι (Fin 3) ℝ) (Y : Matrix κ (Fin 3) ℝ) (I : Fin r → ι) (J : Fin r → κ) : (X * Y.transpose).submatrix I J = X.submatrix I id * (Y.submatrix J id).transpose

theorem BollobasNikiforov.det_submatrix_mul_transpose_eq_zero_of_lt {ι : Type u_3} {κ : Type u_4} {r : ℕ} (hr : 3 < r) (X : Matrix ι (Fin 3) ℝ) (Y : Matrix κ (Fin 3) ℝ) (I : Fin r → ι) (J : Fin r → κ) : ((X * Y.transpose).submatrix I J).det = 0

Square minors of size greater than 3 of a product X * Yᵀ vanish, since the factors have only three columns (rank at most 3).

theorem BollobasNikiforov.det_submatrix_mul_transpose_eq_sum_strictMono {ι : Type u_3} {κ : Type u_4} {r : ℕ} (X : Matrix ι (Fin 3) ℝ) (Y : Matrix κ (Fin 3) ℝ) (I : Fin r → ι) (J : Fin r → κ) : ((X * Y.transpose).submatrix I J).det = ∑ S : StrictMonoFin3 r, (X.submatrix I ↑S).det * (Y.submatrix J ↑S).det

Cauchy–Binet for a product of two three-column real matrices. The sum runs over the strictly increasing maps Fin r → Fin 3 (equivalently, the C(3, r) increasing embeddings, enumerated as the unique empty map, the three constants, Fin.succAbove, and id). For r > 3 both sides are zero.

TN04: product of two 3-column TN matrices

theorem BollobasNikiforov.IsTotallyNonneg.mul_transpose {ι : Type u_3} {κ : Type u_4} [LinearOrder ι] [LinearOrder κ] {X : Matrix ι (Fin 3) ℝ} {Y : Matrix κ (Fin 3) ℝ} (hX : IsTotallyNonneg X) (hY : IsTotallyNonneg Y) : IsTotallyNonneg (X * Y.transpose)

The product X * Yᵀ of two three-column totally nonnegative matrices is totally nonnegative. Size r > 3 minors vanish by rank; smaller minors are nonnegative sums of products of TN minors via Cauchy–Binet.