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.squareSetSubmatrix {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) {X : Finset (Fin m)} {Y : Finset (Fin n)} (hXY : X.card = Y.card) : Matrix (Fin X.card) (Fin X.card) ℚ

Equations

• One or more equations did not get rendered due to their size.

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), (A.squareSetSubmatrix hXY).det ∈ SignType.cast.range)

theorem Matrix.abs_det_reindex_self_self {m n : Type} [DecidableEq m] [Fintype m] [DecidableEq n] [Fintype n] {R : Type} [LinearOrderedCommRing R] (A : Matrix m m R) (e₁ e₂ : m ≃ n) : |((reindex e₁ e₂) A).det| = |A.det|

theorem range_eq_range_iff_exists_comp_equiv {α β γ : Type} {f : α → γ} {g : β → γ} (hf : Function.Injective f) (hg : Function.Injective g) : f.range = g.range ↔ ∃ (e : α ≃ β), f = g ∘ ⇑e

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

theorem Matrix.submatrix_eq_submatrix_reindex {r c n o p q α : Type} [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.