instUsableInSimplexAlgorithmSparseMatrix

Lean4
instance : UsableInSimplexAlgorithm SparseMatrix
    where
  getElem mat i j := mat.data[i]!.getD j 0
  setElem mat i j
    v := if v == 0 then ⟨mat.data.modify i fun row => row.erase j⟩ else ⟨mat.data.modify i fun row => row.insert j v⟩
  getValues
    mat :=
    mat.data.zipIdx.foldl (init := []) fun acc (row, i) =>
      let rowVals := row.toList.map fun (j, v) => (i, j, v)
      rowVals ++ acc
  ofValues {n _ : Nat}
    vals :=
    Id.run
      (do
        let mut data : Array (Std.HashMap Nat Rat) := Array.replicate n ∅
        for ⟨i, j, v⟩ in vals do
          if v != 0 then
            data := data.modify i fun row => row.insert j v
        return ⟨data⟩)
  swapRows mat i j := ⟨mat.data.swapIfInBounds i j⟩
  subtractRow mat i j
    coef :=
    let newData :=
      mat.data.modify j fun row =>
        mat.data[i]!.fold
          (fun cur k val =>
            let newVal := (cur.getD k 0) - coef * val
            if newVal != 0 then cur.insert k newVal else cur.erase k)
          row
    ⟨newData⟩
  divideRow mat i
    coef :=
    let newData : Array (Std.HashMap Nat Rat) :=
      mat.data.modify i fun row => row.fold (fun cur k v => cur.insert k (v / coef)) row
    ⟨newData⟩
Похожие утверждения