OAI/Combinatorics/MatchingCount/Tapes/GuardBits.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.FiniteTrial.guardBits line 20
  2. def OAI.MatchingFPRAS.FiniteTrial.ScaleState.drawGuard line 21
  3. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.drawGuard_law line 24
  4. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.drawGuard_no_certificate line 30
  5. def OAI.MatchingFPRAS.FiniteTrial.guardedBits line 36
  6. def OAI.MatchingFPRAS.FiniteTrial.drawGuarded line 37
  7. lemma OAI.MatchingFPRAS.FiniteTrial.drawGuarded_law line 43
  8. def OAI.MatchingFPRAS.FiniteTrial.guardedBitOutput line 53
  9. lemma OAI.MatchingFPRAS.FiniteTrial.guardedBitOutput_nonneg line 55
  10. theorem OAI.MatchingFPRAS.FiniteTrial.guardedBitOutput_zero line 57
  11. def OAI.MatchingFPRAS.FiniteTrial.guardedAmplifiedBits line 63
  12. def OAI.MatchingFPRAS.FiniteTrial.drawGuardedTrials line 65
  13. lemma OAI.MatchingFPRAS.FiniteTrial.drawGuardedTrials_law line 68
  14. def OAI.MatchingFPRAS.FiniteTrial.guardedAmplifiedOutput line 74
  15. def OAI.MatchingFPRAS.FiniteTrial.guardedAmplifiedBitOutput line 76
  16. lemma OAI.MatchingFPRAS.FiniteTrial.guardedAmplifiedBitOutput_nonneg line 78
  17. lemma OAI.MatchingFPRAS.FiniteTrial.median_eq_of_constant line 83
  18. theorem OAI.MatchingFPRAS.FiniteTrial.guardedAmplifiedBitOutput_zero line 91
  19. def OAI.MatchingFPRAS.FiniteTrial.guardedAccurateBits line 97
  20. theorem OAI.MatchingFPRAS.FiniteTrial.guardedAmplifiedBitOutput_success line 99