OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredPartitions.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Stored balanced partitions with the analyzed sampler law

  1. abbrev OAI.LowSpaceSubsetSum.StoredPartitions.Data line 13
  2. def OAI.LowSpaceSubsetSum.StoredPartitions.run line 15
  3. def OAI.LowSpaceSubsetSum.StoredPartitions.encode line 19
  4. theorem OAI.LowSpaceSubsetSum.StoredPartitions.value line 23
  5. theorem OAI.LowSpaceSubsetSum.StoredPartitions.complete line 31
  6. theorem OAI.LowSpaceSubsetSum.StoredPartitions.source line 37
  7. theorem OAI.LowSpaceSubsetSum.StoredPartitions.work line 49