OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredLeafPreparation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The eight leaf profiles computed from stored index lists

Both prescribed subset sizes use integer division of the stored guesses. The domains are obtained by scanning the stored labels and by reading the eight consecutive background rows.

  1. def OAI.LowSpaceSubsetSum.StoredLeafPreparation.make line 18
  2. def OAI.LowSpaceSubsetSum.StoredLeafPreparation.leaf line 30
  3. def OAI.LowSpaceSubsetSum.StoredLeafPreparation.run line 43
  4. theorem OAI.LowSpaceSubsetSum.StoredLeafPreparation.value line 49
  5. theorem OAI.LowSpaceSubsetSum.StoredLeafPreparation.block_length_le line 75
  6. theorem OAI.LowSpaceSubsetSum.StoredLeafPreparation.leaf_work line 80
  7. theorem OAI.LowSpaceSubsetSum.StoredLeafPreparation.work line 111