OAI/Combinatorics/MatchingCount/Sampling/PairStep.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.Replica.replacePair_at line 15
2. lemma OAI.MatchingFPRAS.Replica.replacePair_idem line 20
3. def OAI.MatchingFPRAS.Replica.pairStep line 29
4. def OAI.MatchingFPRAS.Replica.baseStep line 32
5. lemma OAI.MatchingFPRAS.Replica.local_pairFlow line 35
6. lemma OAI.MatchingFPRAS.Replica.local_baseFlow line 70
7. def OAI.MatchingFPRAS.Replica.localScan line 100
8. theorem OAI.MatchingFPRAS.Replica.localScan_kernel line 106
9. def OAI.MatchingFPRAS.WeightedOptions.drawThen line 145
10. lemma OAI.MatchingFPRAS.WeightedOptions.drawThen_law line 149
11. theorem OAI.MatchingFPRAS.WeightedOptions.drawThen_tv line 154
12. abbrev OAI.MatchingFPRAS.Replica.Update line 177
13. def OAI.MatchingFPRAS.Replica.updates line 179
14. lemma OAI.MatchingFPRAS.Replica.updates_card line 182
15. lemma OAI.MatchingFPRAS.Replica.updates_nonempty line 191
16. def OAI.MatchingFPRAS.Replica.updateKernel line 198
17. lemma OAI.MatchingFPRAS.Replica.pairStep_nonneg line 204
18. lemma OAI.MatchingFPRAS.Replica.pairStep_sum line 212
19. lemma OAI.MatchingFPRAS.Replica.baseStep_nonneg line 220
20. lemma OAI.MatchingFPRAS.Replica.baseStep_sum line 227
21. lemma OAI.MatchingFPRAS.Replica.updateKernel_nonneg line 233
22. lemma OAI.MatchingFPRAS.Replica.updateKernel_sum line 241
23. def OAI.MatchingFPRAS.Replica.scanChoice line 252
24. lemma OAI.MatchingFPRAS.Replica.scanChoice_size line 257
25. lemma OAI.MatchingFPRAS.Replica.scanChoice_law line 262
26. def OAI.MatchingFPRAS.Replica.localSampler line 291
27. lemma OAI.MatchingFPRAS.Replica.localSampler_tv line 297
28. def OAI.MatchingFPRAS.Replica.sampleScan line 340
29. theorem OAI.MatchingFPRAS.Replica.sampleScan_tv line 345
30. def OAI.MatchingFPRAS.Variation.runSample line 372
31. lemma OAI.MatchingFPRAS.Variation.runSample_law line 377
32. theorem OAI.MatchingFPRAS.Variation.runSample_walk_tv line 389