OAI/Combinatorics/LowSpaceSubsetSum/Streams/ReaderInitializationMap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Semantic maps commute with the actual binary-search initialization

  1. theorem OAI.LowSpaceSubsetSum.BinarySlice.search_lo_congr line 12
  2. theorem OAI.LowSpaceSubsetSum.BinarySlice.lower_map line 20
  3. theorem OAI.LowSpaceSubsetSum.BinarySlice.upper_map line 27
  4. theorem OAI.LowSpaceSubsetSum.BinarySlice.range_map line 34
  5. theorem OAI.LowSpaceSubsetSum.SliceModular.forward_map line 47
  6. theorem OAI.LowSpaceSubsetSum.SliceModular.reverse_map line 60
  7. theorem OAI.LowSpaceSubsetSum.FilteredRow.forward_map line 78
  8. theorem OAI.LowSpaceSubsetSum.FilteredRow.reverse_map line 92
  9. theorem OAI.LowSpaceSubsetSum.FilteredStream.key_map line 111
  10. theorem OAI.LowSpaceSubsetSum.FilteredStream.row_map line 117
  11. theorem OAI.LowSpaceSubsetSum.FilteredStream.rowArray_map line 134
  12. theorem OAI.LowSpaceSubsetSum.FilteredStream.initial_tree_map line 147