OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationPreparedTrial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The stopped trial consumes only its stored preparation

  1. abbrev OAI.LowSpaceSubsetSum.RepresentationPreparedTrial.width line 13
  2. theorem OAI.LowSpaceSubsetSum.RepresentationPreparedTrial.family_sizes line 15
  3. def OAI.LowSpaceSubsetSum.RepresentationPreparedTrial.control line 27
  4. def OAI.LowSpaceSubsetSum.RepresentationPreparedTrial.run line 43
  5. theorem OAI.LowSpaceSubsetSum.RepresentationPreparedTrial.value line 55
  6. theorem OAI.LowSpaceSubsetSum.RepresentationPreparedTrial.accepts line 102
  7. theorem OAI.LowSpaceSubsetSum.RepresentationPreparedTrial.sound line 175
  8. theorem OAI.LowSpaceSubsetSum.RepresentationPreparedTrial.work line 184