Documentation

CompPoly.LinearAlgebra.Dense.RowOpsCorrectness

Dense Row-Operation Correctness #

Correctness lemmas for executable dense row operations.

source
theorem CompPoly.DenseMatrix.index_lt_of_lt {F : Type u_1} [Zero F] {M : DenseMatrix F} (hM : M.WellFormed) {row col : ℕ} (hrow : row < M.rows) (hcol : col < M.cols) :
M.index row col < M.data.size
source
theorem CompPoly.DenseMatrix.get_setD_index_same {F : Type u_1} [Zero F] {M : DenseMatrix F} {data : Array F} {row col : ℕ} (hidx : M.index row col < data.size) (value : F) :
(setD data (M.index row col) value).getD (M.index row col) 0 = value
source
theorem CompPoly.DenseMatrix.get_setD_index_ne {F : Type u_1} [Zero F] (M : DenseMatrix F) (data : Array F) {row col row' col' : ℕ} (hcol : col < M.cols) (hcol' : col' < M.cols) (hne : row ≠ row' ∨ col ≠ col') (value : F) :
(setD data (M.index row col) value).getD (M.index row' col') 0 = data.getD (M.index row' col') 0
source
theorem CompPoly.DenseMatrix.get_setD_index_ne_same_row {F : Type u_1} [Zero F] (M : DenseMatrix F) (data : Array F) {row col col' : ℕ} (hcol : col < M.cols) (hcol' : col' < M.cols) (hne : col ≠ col') (value : F) :
(setD data (M.index row col) value).getD (M.index row col') 0 = data.getD (M.index row col') 0
source
theorem CompPoly.DenseMatrix.get_setD_index_ne_same_col {F : Type u_1} [Zero F] (M : DenseMatrix F) (data : Array F) {row row' col : ℕ} (hcol : col < M.cols) (hne : row ≠ row') (value : F) :
(setD data (M.index row col) value).getD (M.index row' col) 0 = data.getD (M.index row' col) 0
source
theorem CompPoly.DenseMatrix.list_foldl_array_size_of_eq {α : Type u_1} {β : Type u_2} (f : Array α → β → Array α) (h : ∀ (data : Array α) (x : β), (f data x).size = data.size) (xs : List β) (data : Array α) :
(List.foldl f data xs).size = data.size
source
theorem CompPoly.DenseMatrix.swapRows_cols {F : Type u_1} [Zero F] (M : DenseMatrix F) (rowA rowB : ℕ) :
(M.swapRows rowA rowB).cols = M.cols
source
theorem CompPoly.DenseMatrix.swapRows_rows {F : Type u_1} [Zero F] (M : DenseMatrix F) (rowA rowB : ℕ) :
(M.swapRows rowA rowB).rows = M.rows
source
theorem CompPoly.DenseMatrix.swapRows_wf {F : Type u_1} [Zero F] {M : DenseMatrix F} (hM : M.WellFormed) (rowA rowB : ℕ) :
(M.swapRows rowA rowB).WellFormed
source
theorem CompPoly.DenseMatrix.swapRows_get_of_row_ne {F : Type u_1} [Zero F] {M : DenseMatrix F} {rowA rowB row col : ℕ} (hcol : col < M.cols) (hA : rowA ≠ row) (hB : rowB ≠ row) :
(M.swapRows rowA rowB).get row col = M.get row col
source
theorem CompPoly.DenseMatrix.swapRows_get_left {F : Type u_1} [Zero F] {M : DenseMatrix F} (hM : M.WellFormed) {rowA rowB col : ℕ} (hrowA : rowA < M.rows) (hcol : col < M.cols) :
(M.swapRows rowA rowB).get rowA col = M.get rowB col
source
theorem CompPoly.DenseMatrix.swapRows_get_right {F : Type u_1} [Zero F] {M : DenseMatrix F} (hM : M.WellFormed) {rowA rowB col : ℕ} (hrowB : rowB < M.rows) (hcol : col < M.cols) :
(M.swapRows rowA rowB).get rowB col = M.get rowA col
source
theorem CompPoly.DenseMatrix.list_forIn_addScaledRow_rows {F : Type u_1} [Field F] (rows : List ℕ) (pivotRow pivotCol : ℕ) (out : DenseMatrix F) :
(forIn rows out fun (row : ℕ) (r : DenseMatrix F) => if row = pivotRow then pure (ForInStep.yield r) else pure (ForInStep.yield (r.addScaledRow row pivotRow (-r.get row pivotCol)))).run.rows = out.rows
source
theorem CompPoly.DenseMatrix.list_forIn_addScaledRow_cols {F : Type u_1} [Field F] (rows : List ℕ) (pivotRow pivotCol : ℕ) (out : DenseMatrix F) :
(forIn rows out fun (row : ℕ) (r : DenseMatrix F) => if row = pivotRow then pure (ForInStep.yield r) else pure (ForInStep.yield (r.addScaledRow row pivotRow (-r.get row pivotCol)))).run.cols = out.cols
source
theorem CompPoly.DenseMatrix.normalizeAndEliminate_cols {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) (pivotRow pivotCol : ℕ) :
(M.normalizeAndEliminate pivotRow pivotCol).cols = M.cols
source
theorem CompPoly.DenseMatrix.normalizeAndEliminate_rows {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) (pivotRow pivotCol : ℕ) :
(M.normalizeAndEliminate pivotRow pivotCol).rows = M.rows
source
theorem CompPoly.DenseMatrix.scaleRow_get_of_row_ne {F : Type u_1} [Field F] {M : DenseMatrix F} {r row col : ℕ} (factor : F) (hcol : col < M.cols) (hneq : r ≠ row) :
(M.scaleRow r factor).get row col = M.get row col
source
theorem CompPoly.DenseMatrix.scaleRow_wf {F : Type u_1} [Field F] {M : DenseMatrix F} (hM : M.WellFormed) (row : ℕ) (factor : F) :
(M.scaleRow row factor).WellFormed
source
theorem CompPoly.DenseMatrix.scaleRow_get_same {F : Type u_1} [Field F] {M : DenseMatrix F} (hM : M.WellFormed) {r col : ℕ} (hr : r < M.rows) (hcol : col < M.cols) (factor : F) :
(M.scaleRow r factor).get r col = factor * M.get r col
source
theorem CompPoly.DenseMatrix.addScaledRow_get_of_row_ne {F : Type u_1} [Field F] {M : DenseMatrix F} {target source row col : ℕ} (factor : F) (hcol : col < M.cols) (hneq : target ≠ row) :
(M.addScaledRow target source factor).get row col = M.get row col
source
theorem CompPoly.DenseMatrix.addScaledRow_wf {F : Type u_1} [Field F] {M : DenseMatrix F} (hM : M.WellFormed) (target source : ℕ) (factor : F) :
(M.addScaledRow target source factor).WellFormed
source
theorem CompPoly.DenseMatrix.addScaledRow_get_same {F : Type u_1} [Field F] {M : DenseMatrix F} (hM : M.WellFormed) {target source col : ℕ} (htarget : target < M.rows) (hcol : col < M.cols) (factor : F) :
(M.addScaledRow target source factor).get target col = M.get target col + factor * M.get source col
source
theorem CompPoly.DenseMatrix.dotRow_ext_rows {F : Type u_1} [Semiring F] {M N : DenseMatrix F} {rowN rowM : ℕ} {v : Array F} (hcols : N.cols = M.cols) (hget : ∀ (col : ℕ), col < M.cols → N.get rowN col = M.get rowM col) :
N.dotRow rowN v = M.dotRow rowM v
source
theorem CompPoly.DenseMatrix.dotRow_scaleRow_same {F : Type u_1} [Field F] {M : DenseMatrix F} (hM : M.WellFormed) {row : ℕ} (hrow : row < M.rows) (factor : F) (v : Array F) :
(M.scaleRow row factor).dotRow row v = factor * M.dotRow row v
source
theorem CompPoly.DenseMatrix.dotRow_addScaledRow_same {F : Type u_1} [Field F] {M : DenseMatrix F} (hM : M.WellFormed) {target source : ℕ} (htarget : target < M.rows) (factor : F) (v : Array F) :
(M.addScaledRow target source factor).dotRow target v = M.dotRow target v + factor * M.dotRow source v
source
theorem CompPoly.DenseMatrix.dotRow_swapRows_left {F : Type u_1} [Semiring F] {M : DenseMatrix F} (hM : M.WellFormed) {rowA rowB : ℕ} (hrowA : rowA < M.rows) (v : Array F) :
(M.swapRows rowA rowB).dotRow rowA v = M.dotRow rowB v
source
theorem CompPoly.DenseMatrix.dotRow_swapRows_right {F : Type u_1} [Semiring F] {M : DenseMatrix F} (hM : M.WellFormed) {rowA rowB : ℕ} (hrowB : rowB < M.rows) (v : Array F) :
(M.swapRows rowA rowB).dotRow rowB v = M.dotRow rowA v
source
theorem CompPoly.DenseMatrix.dotRow_swapRows_of_ne {F : Type u_1} [Semiring F] {M : DenseMatrix F} {rowA rowB row : ℕ} (hrowA : rowA ≠ row) (hrowB : rowB ≠ row) (v : Array F) :
(M.swapRows rowA rowB).dotRow row v = M.dotRow row v
source
theorem CompPoly.DenseMatrix.dotRow_scaleRow_of_ne {F : Type u_1} [Field F] {M : DenseMatrix F} {scale row : ℕ} (factor : F) (hneq : scale ≠ row) (v : Array F) :
(M.scaleRow scale factor).dotRow row v = M.dotRow row v
source
theorem CompPoly.DenseMatrix.dotRow_addScaledRow_of_ne {F : Type u_1} [Field F] {M : DenseMatrix F} {target source row : ℕ} (factor : F) (hneq : target ≠ row) (v : Array F) :
(M.addScaledRow target source factor).dotRow row v = M.dotRow row v
source
theorem CompPoly.DenseMatrix.isHomogeneousSolution_swapRows_of_solution {F : Type u_1} [Field F] {M : DenseMatrix F} {v : Array F} {rowA rowB : ℕ} (hM : M.WellFormed) (hrowA : rowA < M.rows) (hrowB : rowB < M.rows) (hsol : M.IsHomogeneousSolution v) :
(M.swapRows rowA rowB).IsHomogeneousSolution v
source
theorem CompPoly.DenseMatrix.isHomogeneousSolution_scaleRow_of_solution {F : Type u_1} [Field F] {M : DenseMatrix F} {v : Array F} {target : ℕ} (hM : M.WellFormed) (htarget : target < M.rows) (factor : F) (hsol : M.IsHomogeneousSolution v) :
(M.scaleRow target factor).IsHomogeneousSolution v
source
theorem CompPoly.DenseMatrix.isHomogeneousSolution_addScaledRow_of_solution {F : Type u_1} [Field F] {M : DenseMatrix F} {v : Array F} {target source : ℕ} (hM : M.WellFormed) (htarget : target < M.rows) (hsource : source < M.rows) (factor : F) (hsol : M.IsHomogeneousSolution v) :
(M.addScaledRow target source factor).IsHomogeneousSolution v
source
theorem CompPoly.DenseMatrix.isHomogeneousSolution_of_swapRows_solution {F : Type u_1} [Field F] {M : DenseMatrix F} {v : Array F} {rowA rowB : ℕ} (hM : M.WellFormed) (hrowA : rowA < M.rows) (hrowB : rowB < M.rows) (hsol : (M.swapRows rowA rowB).IsHomogeneousSolution v) :
M.IsHomogeneousSolution v
source
theorem CompPoly.DenseMatrix.isHomogeneousSolution_of_scaleRow_solution {F : Type u_1} [Field F] {M : DenseMatrix F} {v : Array F} {target : ℕ} (hM : M.WellFormed) (htarget : target < M.rows) {factor : F} (hfactor : factor ≠ 0) (hsol : (M.scaleRow target factor).IsHomogeneousSolution v) :
M.IsHomogeneousSolution v
source
theorem CompPoly.DenseMatrix.isHomogeneousSolution_of_addScaledRow_solution {F : Type u_1} [Field F] {M : DenseMatrix F} {v : Array F} {target source : ℕ} (hM : M.WellFormed) (htarget : target < M.rows) (hsource : source < M.rows) (hts : target ≠ source) (factor : F) (hsol : (M.addScaledRow target source factor).IsHomogeneousSolution v) :
M.IsHomogeneousSolution v