OAI/Combinatorics/MatchingCount/Graphs/PathStrength.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatchingFPRAS.Switching.sdiff_pair_card line 11
2. theorem OAI.MatchingFPRAS.Switching.relocated_card line 24
3. theorem OAI.MatchingFPRAS.Switching.pair_fill_holeRatio line 29
4. theorem OAI.MatchingFPRAS.Switching.adjacent_hole_fill line 36
5. theorem OAI.MatchingFPRAS.Switching.toggle_small_holes_card line 60
6. theorem OAI.MatchingFPRAS.Switching.normalized_relocation line 69
7. theorem OAI.MatchingFPRAS.Switching.normalized_path_relocation line 199
8. theorem OAI.MatchingFPRAS.Switching.hole_relocation_of_strong_path line 245
9. def OAI.MatchingFPRAS.Switching.pathStrength line 282
10. def OAI.MatchingFPRAS.Switching.bottleneck line 290
11. theorem OAI.MatchingFPRAS.Switching.one_le_bottleneck line 297
12. theorem OAI.MatchingFPRAS.Switching.walk_isChain_of_darts line 304
13. theorem OAI.MatchingFPRAS.Switching.bottleneck_path line 320
14. theorem OAI.MatchingFPRAS.Switching.edgeActivity_mono line 344
15. theorem OAI.MatchingFPRAS.Switching.hole_relocation line 349
16. def OAI.MatchingFPRAS.Switching.erasePair line 365
17. theorem OAI.MatchingFPRAS.Switching.erasePair_apply line 386
18. theorem OAI.MatchingFPRAS.Switching.erasePair_holes line 391
19. theorem OAI.MatchingFPRAS.Switching.withEdge_erasePair line 402
20. theorem OAI.MatchingFPRAS.Switching.erasePair_withEdge line 416