OAI/Combinatorics/EditApproximation/Probability/Amplification.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Independent-copy amplification for the seed passes

The tail estimate is the direct finite-subset argument from Section 8. Independence is used only between copies at a fixed state. The subsequent union bound over states makes no independence assumption between states.

  1. theorem OAI.EditApproximation.independent_failure_subset_bound line 18
  2. theorem OAI.EditApproximation.independent_failure_count_bound line 27
  3. theorem OAI.EditApproximation.independent_failure_count_binary_bound line 54