OAI/Combinatorics/LowSpaceSubsetSum/Word/WordDecisionRound.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Independent fair-word rounds and counter-executed amplification

  1. abbrev OAI.LowSpaceSubsetSum.WordDecisionRound.Words line 13
  2. def OAI.LowSpaceSubsetSum.WordDecisionRound.law line 16
  3. def OAI.LowSpaceSubsetSum.WordDecisionRound.combine line 20
  4. def OAI.LowSpaceSubsetSum.WordDecisionRound.run line 23
  5. theorem OAI.LowSpaceSubsetSum.WordDecisionRound.value line 29
  6. theorem OAI.LowSpaceSubsetSum.WordDecisionRound.sound line 36
  7. theorem OAI.LowSpaceSubsetSum.WordDecisionRound.probability line 44
  8. def OAI.LowSpaceSubsetSum.WordDecisionRound.repeated line 76
  9. theorem OAI.LowSpaceSubsetSum.WordDecisionRound.repeated_sound line 81
  10. theorem OAI.LowSpaceSubsetSum.WordDecisionRound.repeated_probability line 88