OAI/Combinatorics/BooleanFunctions/Amplification.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SquareRootDegree.Amplification.Observation line 15
  2. def OAI.SquareRootDegree.Amplification.ratio line 29
  3. def OAI.SquareRootDegree.Amplification.costFactor line 31
  4. def OAI.SquareRootDegree.Amplification.factor line 33
  5. theorem OAI.SquareRootDegree.Amplification.costFactor_eq line 35
  6. theorem OAI.SquareRootDegree.Amplification.costFactor_pos line 38
  7. theorem OAI.SquareRootDegree.Amplification.factor_gt_one line 42
  8. theorem OAI.SquareRootDegree.Amplification.ratio_improvement line 47
  9. theorem OAI.SquareRootDegree.Amplification.exists_step line 58
  10. theorem OAI.SquareRootDegree.Amplification.identity_variance line 78
  11. def OAI.SquareRootDegree.Amplification.base line 86
  12. theorem OAI.SquareRootDegree.Amplification.base_ratio line 101
  13. theorem OAI.SquareRootDegree.Amplification.exists_iterate line 106
  14. theorem OAI.SquareRootDegree.Amplification.exists_large_ratio line 117