OAI/Combinatorics/MatchingCount/Probability/Marking.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.Variation.imageLaw_instances line 9
2. lemma OAI.MatchingFPRAS.Variation.tv_instances line 13
3. def OAI.MatchingFPRAS.RationalSource.centralEdge line 27
4. def OAI.MatchingFPRAS.RationalSource.probePortion line 29
5. def OAI.MatchingFPRAS.RationalSource.portions line 31
6. lemma OAI.MatchingFPRAS.RationalSource.portions_sum line 33
7. lemma OAI.MatchingFPRAS.RationalSource.portions_nonneg line 36
8. lemma OAI.MatchingFPRAS.RationalSource.bagWeight_pos line 49
9. def OAI.MatchingFPRAS.RationalSource.markingTable line 54
10. lemma OAI.MatchingFPRAS.RationalSource.markingTable_law line 61
11. abbrev OAI.MatchingFPRAS.RationalSource.Marked line 67
12. def OAI.MatchingFPRAS.RationalSource.markedLaw line 70
13. def OAI.MatchingFPRAS.RationalSource.markedSampler line 74
14. lemma OAI.MatchingFPRAS.RationalSource.marking_tv line 86
15. def OAI.MatchingFPRAS.RationalSource.markedSamplerLaw line 104
16. theorem OAI.MatchingFPRAS.RationalSource.markedSampler_tv line 110