Reflection certificates for the echelon decomposition

The list-based certificates for a part of Echelon.Decomposition and their bridge lemmas.

Main definitions

• IsLowerTriangularDiagList: a list of rows is lower triangular with nonzero diagonal.
• IsPivotedList: a list of rows has the given pivot columns.
• pivotOfList: the pivot function corresponding to a given list of pivot columns.

Implementation notes

The two conditions are kept as separate predicates for optimised checks. The pivot cert states that each row is 0 up to its pivot column as the one equation row = List.replicate k 0 ++ d :: suffix, which the kernel checks in one traversal of the row. The lower-triangularity check requires each row to be 0 beyond the diagonal, so it skips the prefix by drop.

Lower triangularity and nonzero diagonal of L

Both conditions read the same suffix of each row, so one sweep certifies them together.

inductive Mathlib.Tactic.Echelon.IsLowerTriangularDiagList {α : Type u_1} [Zero α] : ℕ → ℕ → List (List α) → Prop

c rows starting at row k, each with a nonzero entry at its diagonal position and zeros after it to the end of the row.

• nil {α : Type u_1} [Zero α] {k : ℕ} {rows : List (List α)} : IsLowerTriangularDiagList k 0 rows
• cons {α : Type u_1} [Zero α] {k c : ℕ} {row : List α} {rows : List (List α)} {d : α} (hdrop : List.drop k row = d :: List.replicate c 0) (hd : d ≠ 0) (h : IsLowerTriangularDiagList (k + 1) c rows) : IsLowerTriangularDiagList k (c + 1) (row :: rows)

theorem Mathlib.Tactic.Echelon.getD_of_isLowerTriangularDiagList {α : Type u_1} [Zero α] {k c i : ℕ} {rows : List (List α)} (h : IsLowerTriangularDiagList k c rows) (hi : i < c) : (rows.getD i []).getD (k + i) 0 ≠ 0 ∧ ∀ (j : ℕ), k + i < j → (rows.getD i []).getD j 0 = 0

Lookup specification for IsLowerTriangularDiagList.

theorem Mathlib.Tactic.Echelon.isLowerTriangular_ofLists {α : Type u_1} [Zero α] {m : ℕ} {rows : List (List α)} (h : IsLowerTriangularDiagList 0 m rows) : (Matrix.ofLists m m rows).IsLowerTriangular

theorem Mathlib.Tactic.Echelon.diag_ofLists_ne_zero {α : Type u_1} [Zero α] {m : ℕ} {rows : List (List α)} (h : IsLowerTriangularDiagList 0 m rows) (i : Fin m) : (Matrix.ofLists m m rows).diag i ≠ 0

Pivots of U

inductive Mathlib.Tactic.Echelon.IsPivotedList {α : Type u_1} {n : ℕ} [Zero α] : List (Fin n) → List (List α) → Prop

The rows with a nonzero entry at their pivot columns and zeros before it, then the rows beyond the pivot list (all 0).

• nil {α : Type u_1} {n : ℕ} [Zero α] {rows : List (List α)} (hz : rows = List.map (fun (x : List α) => List.replicate n 0) rows) : IsPivotedList [] rows
• cons {α : Type u_1} {n : ℕ} [Zero α] {k : Fin n} {ks : List (Fin n)} {row : List α} {rows : List (List α)} {d : α} {suffix : List α} (hrow : row = List.replicate (↑k) 0 ++ d :: suffix) (hd : d ≠ 0) (h : IsPivotedList ks rows) : IsPivotedList (k :: ks) (row :: rows)

def Mathlib.Tactic.Echelon.pivotOfList {n : ℕ} (cols : List (Fin n)) (i : ℕ) : WithTop (Fin n)

The pivot function of the list of pivot columns. WithTop (Fin n) is Option (Fin n), so the lookup cols[i]? is the value.

Equations

• Mathlib.Tactic.Echelon.pivotOfList cols i = cols[i]?

theorem Mathlib.Tactic.Echelon.getD_of_isPivotedList {α : Type u_1} {n : ℕ} [Zero α] {cols : List (Fin n)} {rows : List (List α)} (h : IsPivotedList cols rows) (i : ℕ) : (∀ (j : Fin n), ↑j < pivotOfList cols i → (rows.getD i []).getD (↑j) 0 = 0) ∧ ∀ (c : Fin n), pivotOfList cols i = ↑c → (rows.getD i []).getD (↑c) 0 ≠ 0

Lookup specification for IsPivotedList.

theorem Mathlib.Tactic.Echelon.pivotOfList_lt_pivotOfList {n : ℕ} {cols : List (Fin n)} (hsorted : cols.SortedLT) {i j : ℕ} (hij : i < j) (hj : pivotOfList cols j ≠ ⊤) : pivotOfList cols i < pivotOfList cols j

theorem Mathlib.Tactic.Echelon.pivotOfList_mono_of_sortedLT {n : ℕ} {cols : List (Fin n)} (hsorted : cols.SortedLT) : Monotone (pivotOfList cols)

theorem Mathlib.Tactic.Echelon.isPivotedBy_ofLists {α : Type u_1} {n : ℕ} [Zero α] {m : ℕ} {rows : List (List α)} {cols : List (Fin n)} (hsorted : cols.SortedLT) (h : IsPivotedList cols rows) : (Matrix.ofLists m n rows).IsPivotedBy fun (i : Fin m) => pivotOfList cols ↑i