OAI/Combinatorics/LowSpaceSubsetSum/Storage/MeasuredRowCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Explicit scratch for the three searches initializing a stored row

Range endpoints and modular pivots use tail binary search on the retained right array. Only one weight evaluation is live at any time.

  1. def OAI.LowSpaceSubsetSum.MeasuredRowCells.range line 17
  2. theorem OAI.LowSpaceSubsetSum.MeasuredRowCells.range_value line 35
  3. theorem OAI.LowSpaceSubsetSum.MeasuredRowCells.range_cells line 40
  4. def OAI.LowSpaceSubsetSum.MeasuredRowCells.start line 52
  5. theorem OAI.LowSpaceSubsetSum.MeasuredRowCells.start_value line 63
  6. theorem OAI.LowSpaceSubsetSum.MeasuredRowCells.start_cells line 73
  7. def OAI.LowSpaceSubsetSum.MeasuredRowCells.row line 90
  8. theorem OAI.LowSpaceSubsetSum.MeasuredRowCells.row_value line 108
  9. theorem OAI.LowSpaceSubsetSum.MeasuredRowCells.row_cells line 116