OAI/Combinatorics/LowSpaceSubsetSum/Word/WordMeasuredDecision.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Decision rounds with executed random-word generation

The finite-word experiment carries the work and peak storage of seed generation, retained seeds, and the prepared actions.

  1. def OAI.LowSpaceSubsetSum.WordMeasuredDecision.asAction line 18
  2. def OAI.LowSpaceSubsetSum.WordMeasuredDecision.compression line 21
  3. def OAI.LowSpaceSubsetSum.WordMeasuredDecision.representationGenerator line 31
  4. def OAI.LowSpaceSubsetSum.WordMeasuredDecision.representation line 35
  5. theorem OAI.LowSpaceSubsetSum.WordMeasuredDecision.execute_projection line 43
  6. theorem OAI.LowSpaceSubsetSum.WordMeasuredDecision.compression_value line 51
  7. theorem OAI.LowSpaceSubsetSum.WordMeasuredDecision.representation_value line 58
  8. def OAI.LowSpaceSubsetSum.WordMeasuredDecision.round line 68
  9. theorem OAI.LowSpaceSubsetSum.WordMeasuredDecision.round_value line 74
  10. def OAI.LowSpaceSubsetSum.WordMeasuredDecision.repeated line 81
  11. theorem OAI.LowSpaceSubsetSum.WordMeasuredDecision.repeated_value line 86
  12. theorem OAI.LowSpaceSubsetSum.WordMeasuredDecision.sound line 97
  13. theorem OAI.LowSpaceSubsetSum.WordMeasuredDecision.probability line 103