OAI/Combinatorics/LowSpaceSubsetSum/Counting/BinarySlice.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Binary search for the exact eligible slice

Two prefix searches find the half-open interval of occurrences with a fixed primary key. A secondary order within equal primary keys gives the sorted slice needed by modular row initialization. Both searches query the shared array directly, including when the eligible slice is empty.

  1. def OAI.LowSpaceSubsetSum.BinarySlice.lower line 21
  2. def OAI.LowSpaceSubsetSum.BinarySlice.upper line 24
  3. theorem OAI.LowSpaceSubsetSum.BinarySlice.lower_spec line 27
  4. theorem OAI.LowSpaceSubsetSum.BinarySlice.upper_spec line 37
  5. theorem OAI.LowSpaceSubsetSum.BinarySlice.lower_bounded line 47
  6. theorem OAI.LowSpaceSubsetSum.BinarySlice.upper_bounded line 51
  7. theorem OAI.LowSpaceSubsetSum.BinarySlice.ordered line 55
  8. def OAI.LowSpaceSubsetSum.BinarySlice.range line 66
  9. theorem OAI.LowSpaceSubsetSum.BinarySlice.index_spec line 74
  10. theorem OAI.LowSpaceSubsetSum.BinarySlice.slice_eq_filter line 82
  11. theorem OAI.LowSpaceSubsetSum.BinarySlice.slice_key line 157
  12. theorem OAI.LowSpaceSubsetSum.BinarySlice.slice_sorted line 166