OAI/Combinatorics/MatchingCount/Algorithm/GuardProbability.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.FiniteTrial.ScaleState.certificateActivity line 20
2. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.certificateActivity_cast line 23
3. def OAI.MatchingFPRAS.FiniteTrial.ScaleState.certificate line 29
4. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.certificate_cast line 33
5. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.certificate_range line 39
6. theorem OAI.MatchingFPRAS.FiniteTrial.ScaleState.drawOne_certificate_zero line 55
7. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.certificate_mean_lower line 66
8. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.runLaw_tv line 76
9. theorem OAI.MatchingFPRAS.FiniteTrial.ScaleState.guard_success line 91
10. lemma OAI.MatchingFPRAS.Adaptive.Law.iid_all line 132
11. lemma OAI.MatchingFPRAS.Adaptive.Law.iid_no_certificate line 150
12. abbrev OAI.MatchingFPRAS.FiniteTrial.GuardSamples line 187
13. def OAI.MatchingFPRAS.FiniteTrial.guardPass line 189
14. def OAI.MatchingFPRAS.FiniteTrial.guardLaw line 191
15. lemma OAI.MatchingFPRAS.FiniteTrial.guard_failure line 193
16. abbrev OAI.MatchingFPRAS.FiniteTrial.GuardedTrial line 200
17. def OAI.MatchingFPRAS.FiniteTrial.guardedLaw line 202
18. def OAI.MatchingFPRAS.FiniteTrial.guardedOutput line 204
19. lemma OAI.MatchingFPRAS.FiniteTrial.guardedOutput_nonneg line 206
20. theorem OAI.MatchingFPRAS.FiniteTrial.guarded_trial_failure line 212