OAI/Combinatorics/MatchingCount/Probability/OnlineSampleLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatchingFPRAS.OnlineSample.LocalRandom line 10
2. abbrev OAI.MatchingFPRAS.OnlineSample.ScanRandom line 11
3. def OAI.MatchingFPRAS.OnlineSample.localRep line 12
4. def OAI.MatchingFPRAS.OnlineSample.scanRep line 14
5. lemma OAI.MatchingFPRAS.OnlineSample.mean_words line 16
6. lemma OAI.MatchingFPRAS.OnlineSample.mean_local line 21
7. lemma OAI.MatchingFPRAS.OnlineSample.mean_scan line 26
8. lemma OAI.MatchingFPRAS.OnlineSample.mean_scans line 31
9. lemma OAI.MatchingFPRAS.OnlineSample.mean_marks line 36
10. abbrev OAI.MatchingFPRAS.OnlineSample.Random line 44
11. def OAI.MatchingFPRAS.OnlineSample.sampleRep line 45
12. lemma OAI.MatchingFPRAS.OnlineSample.mean_sample line 47
13. lemma OAI.MatchingFPRAS.OnlineSample.mean_many line 53