OAI/Combinatorics/MatchingCount/Graphs/HoleBlocks.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingFPRAS.Subdivision.last_hole_terminal line 9
  2. theorem OAI.MatchingFPRAS.Subdivision.successive_holes_parity line 35
  3. theorem OAI.MatchingFPRAS.Subdivision.sorted_holes_alternate line 61
  4. theorem OAI.MatchingFPRAS.Subdivision.neutral_blocks line 89
  5. structure OAI.MatchingFPRAS.Subdivision.HoleBlocks line 116
  6. def OAI.MatchingFPRAS.Subdivision.HoleBlocks.flatten line 121
  7. def OAI.MatchingFPRAS.Subdivision.HoleBlocks.Parity line 124
  8. theorem OAI.MatchingFPRAS.Subdivision.hole_blocks_exist line 129
  9. theorem OAI.MatchingFPRAS.Subdivision.selectedWeight_hole_product line 151
  10. def OAI.MatchingFPRAS.Subdivision.adjacentProducts line 181
  11. lemma OAI.MatchingFPRAS.Subdivision.adjacentProducts_length line 185
  12. lemma OAI.MatchingFPRAS.Subdivision.adjacentProducts_zip line 192
  13. def OAI.MatchingFPRAS.Subdivision.armPotentials line 199
  14. lemma OAI.MatchingFPRAS.Subdivision.armPotentials_length line 202
  15. lemma OAI.MatchingFPRAS.Subdivision.adjacentProducts_arm line 208
  16. def OAI.MatchingFPRAS.Subdivision.pairedPotentials line 219
  17. lemma OAI.MatchingFPRAS.Subdivision.pairedPotentials_length line 222
  18. theorem OAI.MatchingFPRAS.Subdivision.pairedPotentials_activities line 226
  19. def OAI.MatchingFPRAS.Subdivision.profilePotentials line 237
  20. lemma OAI.MatchingFPRAS.Subdivision.profilePotentials_length line 241
  21. def OAI.MatchingFPRAS.Subdivision.profilePotential line 245
  22. theorem OAI.MatchingFPRAS.Subdivision.profileActivity_vertex_factor line 249
  23. lemma OAI.MatchingFPRAS.Subdivision.duplicate_getElem line 265
  24. lemma OAI.MatchingFPRAS.Subdivision.profile_left line 281
  25. lemma OAI.MatchingFPRAS.Subdivision.profile_center line 293
  26. lemma OAI.MatchingFPRAS.Subdivision.profile_right line 301
  27. theorem OAI.MatchingFPRAS.Subdivision.profile_lower line 312
  28. lemma OAI.MatchingFPRAS.Subdivision.profile_noncentral_lower line 320
  29. lemma OAI.MatchingFPRAS.Subdivision.legValue_antitone line 326
  30. lemma OAI.MatchingFPRAS.Subdivision.legValue_step line 333
  31. lemma OAI.MatchingFPRAS.Subdivision.profile_innermost line 342
  32. def OAI.MatchingFPRAS.Subdivision.vertexPotential line 352
  33. lemma OAI.MatchingFPRAS.Subdivision.vertexPotential_zero line 357
  34. lemma OAI.MatchingFPRAS.Subdivision.vertexPotential_last line 360
  35. theorem OAI.MatchingFPRAS.Subdivision.profile_vertexPotential line 365
  36. def OAI.MatchingFPRAS.Subdivision.internalStrength line 395
  37. lemma OAI.MatchingFPRAS.Subdivision.le_internalStrength line 399
  38. theorem OAI.MatchingFPRAS.Subdivision.internalStrength_incident line 403
  39. theorem OAI.MatchingFPRAS.Subdivision.internalStrength_left_leg line 432
  40. theorem OAI.MatchingFPRAS.Subdivision.internalStrength_right_leg line 439
  41. lemma OAI.MatchingFPRAS.Subdivision.internalStrength_left_antitone line 446
  42. lemma OAI.MatchingFPRAS.Subdivision.internalStrength_right_monotone line 453
  43. lemma OAI.MatchingFPRAS.Subdivision.vertexPotential_pos line 460
  44. lemma OAI.MatchingFPRAS.Subdivision.consumed_left_potential line 469
  45. lemma OAI.MatchingFPRAS.Subdivision.consumed_right_potential line 482