OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredBackgroundBlocks.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Consecutive background blocks from a stored sorted domain

Eight prefix-sum offsets determine the physical array reads. The finite background-color equivalence is used only to prove that these rows are the same blocks as in the finite-partition specification.

  1. def OAI.LowSpaceSubsetSum.StoredBackgroundBlocks.index line 17
  2. theorem OAI.LowSpaceSubsetSum.StoredBackgroundBlocks.index_value line 23
  3. def OAI.LowSpaceSubsetSum.StoredBackgroundBlocks.row line 29
  4. theorem OAI.LowSpaceSubsetSum.StoredBackgroundBlocks.row_length line 33
  5. theorem OAI.LowSpaceSubsetSum.StoredBackgroundBlocks.point_source line 37
  6. theorem OAI.LowSpaceSubsetSum.StoredBackgroundBlocks.row_source line 46
  7. theorem OAI.LowSpaceSubsetSum.StoredBackgroundBlocks.row_source_of_size line 75
  8. def OAI.LowSpaceSubsetSum.StoredBackgroundBlocks.run line 84
  9. theorem OAI.LowSpaceSubsetSum.StoredBackgroundBlocks.run_work line 88