OAI/Combinatorics/LowSpaceSubsetSum/Search/PreparedDecisionRound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A decision round executes both concrete stopped preparations

  1. abbrev OAI.LowSpaceSubsetSum.PreparedDecisionRound.Seed line 14
  2. def OAI.LowSpaceSubsetSum.PreparedDecisionRound.law line 18
  3. def OAI.LowSpaceSubsetSum.PreparedDecisionRound.run line 22
  4. theorem OAI.LowSpaceSubsetSum.PreparedDecisionRound.value line 30
  5. theorem OAI.LowSpaceSubsetSum.PreparedDecisionRound.sound line 37
  6. theorem OAI.LowSpaceSubsetSum.PreparedDecisionRound.probability line 45
  7. theorem OAI.LowSpaceSubsetSum.PreparedDecisionRound.repeated_sound line 78
  8. theorem OAI.LowSpaceSubsetSum.PreparedDecisionRound.repeated_probability line 84