Dense RREF Shape Correctness

Pivot-column and processed-column invariants for dense row reduction.

def CompPoly.DenseMatrix.PivotColumnsShaped {F : Type u_1} [Zero F] [One F] (M : DenseMatrix F) (pivots : Array ℕ) : Prop

Recorded pivot columns have the reduced-column shape expected of RREF.

theorem CompPoly.DenseMatrix.pivotColumnsShaped_empty {F : Type u_1} [Zero F] [One F] (M : DenseMatrix F) : M.PivotColumnsShaped #[]

theorem CompPoly.DenseMatrix.swapRows_preserves_column_shape_of_ne {F : Type u_1} [Zero F] [One F] {M : DenseMatrix F} (hM : M.WellFormed) {rowA rowB pivot oldCol : ℕ} (hrowA : rowA < M.rows) (hrowB : rowB < M.rows) (hcol : oldCol < M.cols) (hA : rowA ≠ pivot) (hB : rowB ≠ pivot) (hshape : ∀ (row : ℕ), row < M.rows → M.get row oldCol = if row = pivot then 1 else 0) (row : ℕ) : row < (M.swapRows rowA rowB).rows → (M.swapRows rowA rowB).get row oldCol = if row = pivot then 1 else 0

theorem CompPoly.DenseMatrix.list_forIn_addScaledRow_get_of_not_mem {F : Type u_1} [Field F] (rows : List ℕ) {out : DenseMatrix F} {row col pivotRow pivotCol : ℕ} (hcol : col < out.cols) (hnot : ¬row ∈ rows) : (forIn rows out fun (r : ℕ) (M : DenseMatrix F) => if r = pivotRow then pure (ForInStep.yield M) else pure (ForInStep.yield (M.addScaledRow r pivotRow (-M.get r pivotCol)))).run.get row col = out.get row col

theorem CompPoly.DenseMatrix.list_forIn_addScaledRow_get_pivotRow {F : Type u_1} [Field F] (rows : List ℕ) {out : DenseMatrix F} {pivotRow pivotCol : ℕ} (hcol : pivotCol < out.cols) (hpivot : out.get pivotRow pivotCol = 1) : (forIn rows out fun (row : ℕ) (M : DenseMatrix F) => if row = pivotRow then pure (ForInStep.yield M) else pure (ForInStep.yield (M.addScaledRow row pivotRow (-M.get row pivotCol)))).run.get pivotRow pivotCol = 1

theorem CompPoly.DenseMatrix.list_forIn_addScaledRow_get_row_mem {F : Type u_1} [Field F] (rows : List ℕ) {out : DenseMatrix F} {row pivotRow pivotCol : ℕ} (hout : out.WellFormed) (hpivotRow : pivotRow < out.rows) (hcol : pivotCol < out.cols) (hpivot : out.get pivotRow pivotCol = 1) (hrows : ∀ (r : ℕ), r ∈ rows → r < out.rows) (hnodup : rows.Nodup) (hmem : row ∈ rows) (hne : row ≠ pivotRow) : (forIn rows out fun (r : ℕ) (M : DenseMatrix F) => if r = pivotRow then pure (ForInStep.yield M) else pure (ForInStep.yield (M.addScaledRow r pivotRow (-M.get r pivotCol)))).run.get row pivotCol = 0

theorem CompPoly.DenseMatrix.list_forIn_addScaledRow_get_of_source_zero {F : Type u_1} [Field F] (rows : List ℕ) {out : DenseMatrix F} {row pivotRow oldCol pivotCol : ℕ} (hout : out.WellFormed) (hcol : oldCol < out.cols) (hrows : ∀ (r : ℕ), r ∈ rows → r < out.rows) (hsource : out.get pivotRow oldCol = 0) : (forIn rows out fun (r : ℕ) (M : DenseMatrix F) => if r = pivotRow then pure (ForInStep.yield M) else pure (ForInStep.yield (M.addScaledRow r pivotRow (-M.get r pivotCol)))).run.get row oldCol = out.get row oldCol

theorem CompPoly.DenseMatrix.normalizeAndEliminate_get_pivot {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : DenseMatrix F} (hM : M.WellFormed) {pivotRow pivotCol : ℕ} (hpivotRow : pivotRow < M.rows) (hpivotCol : pivotCol < M.cols) (hpivot : M.get pivotRow pivotCol ≠ 0) : (M.normalizeAndEliminate pivotRow pivotCol).get pivotRow pivotCol = 1

theorem CompPoly.DenseMatrix.normalizeAndEliminate_get_row_pivot {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : DenseMatrix F} (hM : M.WellFormed) {pivotRow pivotCol row : ℕ} (hpivotRow : pivotRow < M.rows) (hpivotCol : pivotCol < M.cols) (hrow : row < M.rows) (hne : row ≠ pivotRow) (hpivot : M.get pivotRow pivotCol ≠ 0) : (M.normalizeAndEliminate pivotRow pivotCol).get row pivotCol = 0

theorem CompPoly.DenseMatrix.normalizeAndEliminate_get_of_pivotRow_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : DenseMatrix F} (hM : M.WellFormed) {pivotRow pivotCol oldCol row : ℕ} (hpivotRow : pivotRow < M.rows) (holdCol : oldCol < M.cols) (hpivotZero : M.get pivotRow oldCol = 0) : (M.normalizeAndEliminate pivotRow pivotCol).get row oldCol = M.get row oldCol

theorem CompPoly.DenseMatrix.rrefLoop_pivots_size_le_rows {F : Type u_1} [Field F] [BEq F] (fuel col row : ℕ) (M : DenseMatrix F) (pivots : Array ℕ) : row ≤ M.rows → (rrefLoop fuel col row M pivots).pivots.size ≤ pivots.size + (M.rows - row)

theorem CompPoly.DenseMatrix.rref_pivots_size_le_rows {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) : M.rref.pivots.size ≤ M.rows

def CompPoly.DenseMatrix.PivotColumnsBefore (pivots : Array ℕ) (col : ℕ) : Prop

All recorded pivot columns are strictly before the current scan column.

def CompPoly.DenseMatrix.PivotColumnsStrict (pivots : Array ℕ) : Prop

Pivot columns are strictly increasing in pivot-row order.

theorem CompPoly.DenseMatrix.pivotColumnsBefore_empty (col : ℕ) : PivotColumnsBefore #[] col

theorem CompPoly.DenseMatrix.pivotColumnsStrict_empty : PivotColumnsStrict #[]

theorem CompPoly.DenseMatrix.pivotColumnsBefore_mono {pivots : Array ℕ} {col next : ℕ} (h : PivotColumnsBefore pivots col) (hcol : col < next) : PivotColumnsBefore pivots next

theorem CompPoly.DenseMatrix.pivotColumnsBefore_push {pivots : Array ℕ} {col next : ℕ} (h : PivotColumnsBefore pivots col) (hcol : col < next) : PivotColumnsBefore (pivots.push col) next

theorem CompPoly.DenseMatrix.pivotColumnsStrict_push {pivots : Array ℕ} {col : ℕ} (hstrict : PivotColumnsStrict pivots) (hbefore : PivotColumnsBefore pivots col) : PivotColumnsStrict (pivots.push col)

theorem CompPoly.DenseMatrix.pivotColumnsStrict_getD_ne {pivots : Array ℕ} (hstrict : PivotColumnsStrict pivots) {i j : ℕ} (hi : i < pivots.size) (hj : j < pivots.size) (hne : i ≠ j) : pivots.getD i 0 ≠ pivots.getD j 0

theorem CompPoly.DenseMatrix.rrefLoop_pivots_getD_lt_cols {F : Type u_1} [Field F] [BEq F] (fuel col row : ℕ) (M : DenseMatrix F) (pivots : Array ℕ) : (∀ (i : ℕ), i < pivots.size → pivots.getD i 0 < M.cols) → ∀ (i : ℕ), i < (rrefLoop fuel col row M pivots).pivots.size → (rrefLoop fuel col row M pivots).pivots.getD i 0 < M.cols

theorem CompPoly.DenseMatrix.rref_pivots_getD_lt_cols {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) (i : ℕ) : i < M.rref.pivots.size → M.rref.pivots.getD i 0 < M.cols

theorem CompPoly.DenseMatrix.rrefLoop_pivotColumnsStrict {F : Type u_1} [Field F] [BEq F] (fuel col row : ℕ) (M : DenseMatrix F) (pivots : Array ℕ) : PivotColumnsBefore pivots col → PivotColumnsStrict pivots → PivotColumnsStrict (rrefLoop fuel col row M pivots).pivots

theorem CompPoly.DenseMatrix.rref_pivotColumnsStrict {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) : PivotColumnsStrict M.rref.pivots

theorem CompPoly.DenseMatrix.rrefLoop_pivotColumnsShaped {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (fuel col row : ℕ) (M : DenseMatrix F) (pivots : Array ℕ) : M.WellFormed → row = pivots.size → PivotColumnsBefore pivots col → M.PivotColumnsShaped pivots → (rrefLoop fuel col row M pivots).matrix.PivotColumnsShaped (rrefLoop fuel col row M pivots).pivots

theorem CompPoly.DenseMatrix.rref_pivotColumnsShaped {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : DenseMatrix F) (hM : M.WellFormed) : M.rref.matrix.PivotColumnsShaped M.rref.pivots

def CompPoly.DenseMatrix.ProcessedColumnsZeroBelow {F : Type u_1} [Zero F] (M : DenseMatrix F) (activeRow col : ℕ) : Prop

All rows at or below the active pivot row are zero in already-scanned columns.

theorem CompPoly.DenseMatrix.processedColumnsZeroBelow_pivot_step {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : DenseMatrix F} (hM : M.WellFormed) {row col pivotRow : ℕ} (hrow : row < M.rows) (hcol : col < M.cols) (hpivotLt : pivotRow < M.rows) (hpivotGe : row ≤ pivotRow) (hpivotSwap : (M.swapRows pivotRow row).get row col ≠ 0) (hproc : M.ProcessedColumnsZeroBelow row col) : ((M.swapRows pivotRow row).normalizeAndEliminate row col).ProcessedColumnsZeroBelow (row + 1) (col + 1)

theorem CompPoly.DenseMatrix.rrefLoop_processedColumnsZeroBelow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (fuel col row : ℕ) (M : DenseMatrix F) (pivots : Array ℕ) : M.WellFormed → row = pivots.size → row ≤ M.rows → M.cols ≤ col + fuel → M.ProcessedColumnsZeroBelow row col → (rrefLoop fuel col row M pivots).matrix.ProcessedColumnsZeroBelow (rrefLoop fuel col row M pivots).pivots.size M.cols

theorem CompPoly.DenseMatrix.rref_processedColumnsZeroBelow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : DenseMatrix F) (hM : M.WellFormed) : M.rref.matrix.ProcessedColumnsZeroBelow M.rref.pivots.size M.cols