Documentation

CompPoly.LinearAlgebra.Dense.RrefSemantics

Dense RREF Semantic Correctness #

Semantic preservation and reflection lemmas for dense row reduction.

source
def CompPoly.DenseMatrix.findPivotRowStep {F : Type u_1} [Zero F] [BEq F] (M : DenseMatrix F) (col : ℕ) (out : Option ℕ) (row : ℕ) :
Option ℕ
Instances For
    source
    theorem CompPoly.DenseMatrix.list_forIn_yield_eq_foldl {α : Type u_1} {β : Type u_2} (xs : List α) (init : β) (f : β → α → β) :
    (forIn xs init fun (x : α) (acc : β) => pure (ForInStep.yield (f acc x))).run = List.foldl f init xs
    source
    theorem CompPoly.DenseMatrix.findPivotRowStep_fold_some {F : Type u_1} [Zero F] [BEq F] (M : DenseMatrix F) (col : ℕ) (xs : List ℕ) (pivot : ℕ) :
    List.foldl (M.findPivotRowStep col) (some pivot) xs = some pivot
    source
    theorem CompPoly.DenseMatrix.list_forIn_findPivotRowStep_eq_foldl {F : Type u_1} [Zero F] [BEq F] (M : DenseMatrix F) (col : ℕ) (xs : List ℕ) (out : Option ℕ) :
    (forIn xs out fun (row : ℕ) (out : Option ℕ) => if out = none ∧ (M.get row col == 0) = false then pure (ForInStep.yield (some row)) else pure (ForInStep.yield out)).run = List.foldl (M.findPivotRowStep col) out xs
    source
    theorem CompPoly.DenseMatrix.findPivotRow_fold_mem {F : Type u_1} [Zero F] [BEq F] (M : DenseMatrix F) (col : ℕ) {xs : List ℕ} {pivot : ℕ} (h : List.foldl (M.findPivotRowStep col) none xs = some pivot) :
    pivot ∈ xs
    source
    theorem CompPoly.DenseMatrix.findPivotRow_fold_get_ne_zero {F : Type u_1} [Zero F] [BEq F] (M : DenseMatrix F) (col : ℕ) {xs : List ℕ} {pivot : ℕ} (h : List.foldl (M.findPivotRowStep col) none xs = some pivot) :
    (M.get pivot col == 0) = false
    source
    theorem CompPoly.DenseMatrix.findPivotRow_fold_none_get_eq_zero {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] (M : DenseMatrix F) (col : ℕ) {xs : List ℕ} (h : List.foldl (M.findPivotRowStep col) none xs = none) {row : ℕ} (hrow : row ∈ xs) :
    M.get row col = 0
    source
    theorem CompPoly.DenseMatrix.findPivotRow_eq_fold {F : Type u_1} [Zero F] [BEq F] (M : DenseMatrix F) (start col : ℕ) :
    M.findPivotRow start col = List.foldl (M.findPivotRowStep col) none (List.range' start (M.rows - start))
    source
    theorem CompPoly.DenseMatrix.findPivotRow_some_lt {F : Type u_1} [Zero F] [BEq F] {M : DenseMatrix F} {start col pivot : ℕ} (h : M.findPivotRow start col = some pivot) :
    pivot < M.rows
    source
    theorem CompPoly.DenseMatrix.findPivotRow_some_ge {F : Type u_1} [Zero F] [BEq F] {M : DenseMatrix F} {start col pivot : ℕ} (h : M.findPivotRow start col = some pivot) :
    start ≤ pivot
    source
    theorem CompPoly.DenseMatrix.findPivotRow_some_ne_zero {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] {M : DenseMatrix F} {start col pivot : ℕ} (h : M.findPivotRow start col = some pivot) :
    M.get pivot col ≠ 0
    source
    theorem CompPoly.DenseMatrix.findPivotRow_none_get_eq_zero {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] {M : DenseMatrix F} {start col row : ℕ} (h : M.findPivotRow start col = none) (hstart : start ≤ row) (hrow : row < M.rows) :
    M.get row col = 0
    source
    theorem CompPoly.DenseMatrix.list_forIn_addScaledRow_wf {F : Type u_1} [Field F] (rows : List ℕ) {out : DenseMatrix F} (pivotRow pivotCol : ℕ) (hout : out.WellFormed) :
    (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.WellFormed
    source
    theorem CompPoly.DenseMatrix.normalizeAndEliminate_wf {F : Type u_1} [Field F] [BEq F] {M : DenseMatrix F} (hM : M.WellFormed) (pivotRow pivotCol : ℕ) :
    (M.normalizeAndEliminate pivotRow pivotCol).WellFormed
    source
    theorem CompPoly.DenseMatrix.list_forIn_addScaledRow_solution_of_solution {F : Type u_1} [Field F] (rows : List ℕ) {out : DenseMatrix F} {v : Array F} (pivotRow pivotCol : ℕ) (hpivot : pivotRow < out.rows) (hout : out.WellFormed) (hsol : out.IsHomogeneousSolution v) :
    (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.IsHomogeneousSolution v
    source
    theorem CompPoly.DenseMatrix.list_forIn_addScaledRow_solution_reflect {F : Type u_1} [Field F] (rows : List ℕ) {out : DenseMatrix F} {v : Array F} (pivotRow pivotCol : ℕ) (hpivot : pivotRow < out.rows) (hout : out.WellFormed) (hsol : (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.IsHomogeneousSolution v) :
    out.IsHomogeneousSolution v
    source
    theorem CompPoly.DenseMatrix.isHomogeneousSolution_normalizeAndEliminate_of_solution {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : DenseMatrix F} {v : Array F} (hM : M.WellFormed) {pivotRow pivotCol : ℕ} (hpivotRow : pivotRow < M.rows) (hsol : M.IsHomogeneousSolution v) :
    (M.normalizeAndEliminate pivotRow pivotCol).IsHomogeneousSolution v
    source
    theorem CompPoly.DenseMatrix.isHomogeneousSolution_of_normalizeAndEliminate_solution {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : DenseMatrix F} {v : Array F} (hM : M.WellFormed) {pivotRow pivotCol : ℕ} (hpivotRow : pivotRow < M.rows) (hpivot : M.get pivotRow pivotCol ≠ 0) (hsol : (M.normalizeAndEliminate pivotRow pivotCol).IsHomogeneousSolution v) :
    M.IsHomogeneousSolution v
    source
    theorem CompPoly.DenseMatrix.rrefLoop_cols {F : Type u_1} [Field F] [BEq F] (fuel col row : ℕ) (M : DenseMatrix F) (pivots : Array ℕ) :
    (rrefLoop fuel col row M pivots).matrix.cols = M.cols
    source
    theorem CompPoly.DenseMatrix.rrefLoop_rows {F : Type u_1} [Field F] [BEq F] (fuel col row : ℕ) (M : DenseMatrix F) (pivots : Array ℕ) :
    (rrefLoop fuel col row M pivots).matrix.rows = M.rows
    source
    theorem CompPoly.DenseMatrix.rref_cols {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) :
    M.rref.matrix.cols = M.cols
    source
    theorem CompPoly.DenseMatrix.rref_rows {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) :
    M.rref.matrix.rows = M.rows
    source
    theorem CompPoly.DenseMatrix.rrefLoop_wf {F : Type u_1} [Field F] [BEq F] (fuel col row : ℕ) (M : DenseMatrix F) (pivots : Array ℕ) :
    M.WellFormed → (rrefLoop fuel col row M pivots).matrix.WellFormed
    source
    theorem CompPoly.DenseMatrix.rref_wf {F : Type u_1} [Field F] [BEq F] {M : DenseMatrix F} (hM : M.WellFormed) :
    M.rref.matrix.WellFormed
    source
    theorem CompPoly.DenseMatrix.isHomogeneousSolution_rrefLoop_of_solution {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (fuel col row : ℕ) (M : DenseMatrix F) (pivots : Array ℕ) {v : Array F} :
    M.WellFormed → M.IsHomogeneousSolution v → (rrefLoop fuel col row M pivots).matrix.IsHomogeneousSolution v
    source
    theorem CompPoly.DenseMatrix.isHomogeneousSolution_rref {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : DenseMatrix F} (hM : M.WellFormed) {v : Array F} (hsol : M.IsHomogeneousSolution v) :
    M.rref.matrix.IsHomogeneousSolution v
    source
    theorem CompPoly.DenseMatrix.isHomogeneousSolution_of_rrefLoop_solution {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (fuel col row : ℕ) (M : DenseMatrix F) (pivots : Array ℕ) {v : Array F} :
    M.WellFormed → (rrefLoop fuel col row M pivots).matrix.IsHomogeneousSolution v → M.IsHomogeneousSolution v
    source
    theorem CompPoly.DenseMatrix.isHomogeneousSolution_of_rref {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : DenseMatrix F} (hM : M.WellFormed) {v : Array F} (hsol : M.rref.matrix.IsHomogeneousSolution v) :
    M.IsHomogeneousSolution v