Total Unimodularity Test

This file provides means to (computably) test total unimodularity of small matrices.

def Matrix.testTotallyUnimodular {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : Bool

Formally verified algorithm for testing total unimodularity.

Equations

• A.testTotallyUnimodular = decide (∀ k ≤ m ⊓ n, ∀ (x : Fin k → Fin m) (y : Fin k → Fin n), (A.submatrix x y).det ∈ SignType.cast.range)

theorem Matrix.isTotallyUnimodular_of_aux_le {m n : ℕ} {A : Matrix (Fin m) (Fin n) ℚ} (hA : ∀ k ≤ m, ∀ (x : Fin k → Fin m) (y : Fin k → Fin n), (A.submatrix x y).det ∈ SignType.cast.range) : A.IsTotallyUnimodular

theorem Matrix.isTotallyUnimodular_of_testTotallyUnimodular {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : A.testTotallyUnimodular = true → A.IsTotallyUnimodular

theorem Matrix.testTotallyUnimodular_eq_isTotallyUnimodular {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : A.testTotallyUnimodular = true ↔ A.IsTotallyUnimodular

instance instDecidableIsTotallyUnimodularFinRat_seymour {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : Decidable A.IsTotallyUnimodular

Equations

• instDecidableIsTotallyUnimodularFinRat_seymour A = decidable_of_iff (A.testTotallyUnimodular = true) ⋯

theorem filter_length_card {n : ℕ} (s : Finset (Fin n)) : (List.filter (fun (x : Fin n) => decide (x ∈ s)) (List.finRange n)).length = s.card

def Matrix.testTotallyUnimodularFast {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : Bool

Faster algorithm for testing total unimodularity without permutation with pending formal guarantees.

Equations

• A.testTotallyUnimodularFast = decide (∀ (X : Finset (Fin m)) (Y : Finset (Fin n)) (hXY : X.card = Y.card), (Matrix.squareSetSubmatrix✝ A hXY).det ∈ SignType.cast.range)

theorem range_of_list_get {α : Type u_1} [DecidableEq α] {n : ℕ} {s : List α} (hn : n = s.length) : (fun (x : Fin n) => s[x]).range = ↑s.toFinset

theorem Matrix.submatrix_eq_submatrix_reindex {r : Type u_1} {c : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {q : Type u_6} {α : Type u_7} [DecidableEq r] [Fintype r] [DecidableEq c] [Fintype c] [DecidableEq n] [Fintype n] [DecidableEq o] [Fintype o] [DecidableEq p] [Fintype p] [DecidableEq q] [Fintype q] {f₁ : n → r} {g₁ : o → c} {f₂ : p → r} {g₂ : q → c} (A : Matrix r c α) (hf₁ : Function.Injective f₁) (hg₁ : Function.Injective g₁) (hf₂ : Function.Injective f₂) (hg₂ : Function.Injective g₂) (hff : f₁.range = f₂.range) (hgg : g₁.range = g₂.range) : ∃ (e₁ : p ≃ n) (e₂ : q ≃ o), A.submatrix f₁ g₁ = (reindex e₁ e₂) (A.submatrix f₂ g₂)

theorem Matrix.isTotallyUnimodular_of_testTotallyUnimodularFast {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : A.testTotallyUnimodularFast = true → A.IsTotallyUnimodular

A fast version of Matrix.testTotallyUnimodular which doesn't test every permutation.