OAI/Combinatorics/LowSpaceSubsetSum/Storage/MeasuredPivotCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Constant-retention binary-search scratch

The search retains one pair of interval endpoints, one midpoint, and the scratch of a single predicate invocation. The peak accumulator does not retain earlier intervals.

  1. def OAI.LowSpaceSubsetSum.MeasuredPivotCells.step line 16
  2. theorem OAI.LowSpaceSubsetSum.MeasuredPivotCells.step_value line 28
  3. theorem OAI.LowSpaceSubsetSum.MeasuredPivotCells.step_cells line 33
  4. def OAI.LowSpaceSubsetSum.MeasuredPivotCells.loop line 41
  5. theorem OAI.LowSpaceSubsetSum.MeasuredPivotCells.loop_value line 48
  6. theorem OAI.LowSpaceSubsetSum.MeasuredPivotCells.loop_cells line 56
  7. def OAI.LowSpaceSubsetSum.MeasuredPivotCells.search line 66
  8. theorem OAI.LowSpaceSubsetSum.MeasuredPivotCells.search_value line 68
  9. theorem OAI.LowSpaceSubsetSum.MeasuredPivotCells.search_cells line 71