OAI/Combinatorics/MatchingCount/Graphs/Profile.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Subdivision.valid_step_eq_iff line 10
  2. lemma OAI.MatchingFPRAS.Subdivision.valid_eq_iff_zero line 27
  3. theorem OAI.MatchingFPRAS.Subdivision.broken_unique line 38
  4. def OAI.MatchingFPRAS.Subdivision.profile line 48
  5. theorem OAI.MatchingFPRAS.Subdivision.profile_length line 52
  6. def OAI.MatchingFPRAS.Subdivision.profileActivity line 55
  7. theorem OAI.MatchingFPRAS.Subdivision.profileActivity_ofFn line 58
  8. theorem OAI.MatchingFPRAS.Subdivision.exact_profile_weight line 65
  9. def OAI.MatchingFPRAS.Subdivision.Uses line 79
  10. def OAI.MatchingFPRAS.Subdivision.FamilyHoles line 82
  11. def OAI.MatchingFPRAS.Subdivision.broken line 88
  12. lemma OAI.MatchingFPRAS.Subdivision.mem_broken line 92
  13. def OAI.MatchingFPRAS.Subdivision.residualHoles line 97
  14. lemma OAI.MatchingFPRAS.Subdivision.mem_residualHoles line 102
  15. theorem OAI.MatchingFPRAS.Subdivision.residualHoles_independent line 108
  16. def OAI.MatchingFPRAS.Subdivision.LogicalHoles line 124
  17. def OAI.MatchingFPRAS.Subdivision.extract line 130
  18. lemma OAI.MatchingFPRAS.Subdivision.intact_uses line 135
  19. theorem OAI.MatchingFPRAS.Subdivision.extract_legal line 141
  20. def OAI.MatchingFPRAS.Subdivision.rebuild line 174
  21. lemma OAI.MatchingFPRAS.Subdivision.rebuild_uses line 179
  22. theorem OAI.MatchingFPRAS.Subdivision.rebuild_legal line 189
  23. theorem OAI.MatchingFPRAS.Subdivision.rebuild_extract line 230
  24. theorem OAI.MatchingFPRAS.Subdivision.extract_rebuild line 244
  25. def OAI.MatchingFPRAS.Subdivision.deletionEquiv line 255
  26. def OAI.MatchingFPRAS.Subdivision.realHolePartition line 267
  27. def OAI.MatchingFPRAS.Subdivision.logicalHolePartition line 274
  28. def OAI.MatchingFPRAS.Subdivision.deletionConstant line 281
  29. theorem OAI.MatchingFPRAS.Subdivision.deletion_weight line 286
  30. theorem OAI.MatchingFPRAS.Subdivision.deletion_partition_identity line 306
  31. theorem OAI.MatchingFPRAS.Subdivision.selectedWeight_vertex_factor line 326
  32. theorem OAI.MatchingFPRAS.Subdivision.valid_interval line 363
  33. theorem OAI.MatchingFPRAS.Subdivision.first_hole_terminal line 378