OAI/Combinatorics/MatchingCount/Graphs/PM.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatchingFPRAS.Enlargement.SourcePM line 19
2. lemma OAI.MatchingFPRAS.Enlargement.sourceVertex_card_ge line 24
3. theorem OAI.MatchingFPRAS.Enlargement.source_ladder_sampling line 27
4. def OAI.MatchingFPRAS.Subdivision.probeHoles line 54
5. def OAI.MatchingFPRAS.Subdivision.probeWord line 57
6. lemma OAI.MatchingFPRAS.Subdivision.probeWord_valid line 60
7. lemma OAI.MatchingFPRAS.Subdivision.probeWord_first line 77
8. lemma OAI.MatchingFPRAS.Subdivision.probeWord_last line 80
9. lemma OAI.MatchingFPRAS.Subdivision.probeHoles_nonempty line 83
10. lemma OAI.MatchingFPRAS.Subdivision.probeWord_unique line 86
11. lemma OAI.MatchingFPRAS.Subdivision.probe_weight line 90
12. def OAI.MatchingFPRAS.Subdivision.singleProbeHoles line 115
13. lemma OAI.MatchingFPRAS.Subdivision.broken_singleProbe line 118
14. lemma OAI.MatchingFPRAS.Subdivision.singleProbe_word line 123
15. lemma OAI.MatchingFPRAS.Subdivision.residual_singleProbe line 127
16. def OAI.MatchingFPRAS.Subdivision.insertProbe line 136
17. lemma OAI.MatchingFPRAS.Subdivision.insertProbe_uses line 141
18. lemma OAI.MatchingFPRAS.Subdivision.insertProbe_family line 149
19. lemma OAI.MatchingFPRAS.Subdivision.singleProbe_deletionConstant line 182
20. theorem OAI.MatchingFPRAS.Subdivision.singleProbe_partition line 198
21. lemma OAI.MatchingFPRAS.Representation.forbidden_endpoint_redundant line 242
22. lemma OAI.MatchingFPRAS.Representation.logical_partition_redundant line 256
23. theorem OAI.MatchingFPRAS.Enlargement.source_probe_partition line 279
24. theorem OAI.MatchingFPRAS.Enlargement.source_probe_ratio line 294