OAI/Combinatorics/EditApproximation/Probability/FiniteSeedFinal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The final fresh draw selects the coordinate of the actual incoming seed. This keeps the dependence of the finite draw type on that table explicit.

  1. def OAI.EditApproximation.freshSeedValue line 22
  2. theorem OAI.EditApproximation.freshSeed_bad_probability line 25
  3. theorem OAI.EditApproximation.freshSeed_good_excess line 37
  4. theorem OAI.EditApproximation.freshSeed_answer_accuracy line 62