OAI/Combinatorics/CycleDecomposition/Routing.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ErdosGallai.CutExpansion line 17
  2. lemma OAI.ErdosGallai.boundary_sym2_injective line 21
  3. lemma OAI.ErdosGallai.deleted_boundary_card_le line 32
  4. theorem OAI.ErdosGallai.routing_union_growth_step_of_boundary line 42
  5. theorem OAI.ErdosGallai.routing_union_growth_step line 121
  6. def OAI.ErdosGallai.avoidGraph line 142
  7. def OAI.ErdosGallai.walkBall line 150
  8. lemma OAI.ErdosGallai.mem_walkBall line 154
  9. lemma OAI.ErdosGallai.root_mem_walkBall line 159
  10. lemma OAI.ErdosGallai.walkBall_mono line 163
  11. lemma OAI.ErdosGallai.walk_avoids_end line 169
  12. lemma OAI.ErdosGallai.ball_avoids line 175
  13. lemma OAI.ErdosGallai.walkBall_step line 182
  14. def OAI.ErdosGallai.rootBallUnion line 189
  15. lemma OAI.ErdosGallai.rootBallUnion_mono_time line 193
  16. lemma OAI.ErdosGallai.roots_subset_rootBallUnion line 198
  17. theorem OAI.ErdosGallai.rootBallUnion_growth_step line 203
  18. theorem OAI.ErdosGallai.rootBallUnion_growth_block line 234
  19. lemma OAI.ErdosGallai.rootBallUnion_halve line 278
  20. theorem OAI.ErdosGallai.rootBallUnion_extract_root line 303
  21. lemma OAI.ErdosGallai.CutExpansion.le_order line 349
  22. def OAI.ErdosGallai.routingG line 364
  23. def OAI.ErdosGallai.routingDepth line 366
  24. def OAI.ErdosGallai.routingLength line 368
  25. lemma OAI.ErdosGallai.routingG_growth line 370
  26. lemma OAI.ErdosGallai.le_two_pow_routingDepth line 417
  27. theorem OAI.ErdosGallai.routing_large_root_ball line 425
  28. def OAI.ErdosGallai.incidentEdges line 459
  29. lemma OAI.ErdosGallai.incidentEdges_union line 462
  30. lemma OAI.ErdosGallai.incidentEdges_union_card_le line 466
  31. lemma OAI.ErdosGallai.incidentEdges_sum_le line 471
  32. lemma OAI.ErdosGallai.incidentEdges_path_start_le_one line 486
  33. lemma OAI.ErdosGallai.incidentEdges_path_end_le_one line 498
  34. lemma OAI.ErdosGallai.incidentEdges_walk_eq_empty_of_not_mem line 503
  35. lemma OAI.ErdosGallai.incidentEdges_path_le_two line 511
  36. lemma OAI.ErdosGallai.deleted_boundary_card_le_incidents line 525
  37. lemma OAI.ErdosGallai.walkBall_growth_of_incidents line 546
  38. lemma OAI.ErdosGallai.walkBall_large_of_incidents line 567
  39. lemma OAI.ErdosGallai.exists_short_avoiding_path line 603
  40. lemma OAI.ErdosGallai.two_routingG_le_length line 633
  41. lemma OAI.ErdosGallai.routingLength_bounds line 637
  42. lemma OAI.ErdosGallai.routing_budget line 660
  43. def OAI.ErdosGallai.saturated line 685
  44. lemma OAI.ErdosGallai.saturated_card_le line 689
  45. def OAI.ErdosGallai.pathInterior line 701
  46. lemma OAI.ErdosGallai.pathInterior_card_le line 704
  47. lemma OAI.ErdosGallai.avoidGraph_le line 714
  48. lemma OAI.ErdosGallai.walk_avoids_support line 717
  49. lemma OAI.ErdosGallai.walk_avoids_edges line 724
  50. lemma OAI.ErdosGallai.exists_short_path_with_avoidance line 732
  51. lemma OAI.ErdosGallai.route_degree_update line 745
  52. def OAI.ErdosGallai.endpointLoad line 783
  53. lemma OAI.ErdosGallai.endpointLoad_mono line 786
  54. lemma OAI.ErdosGallai.endpointLoad_insert line 790
  55. lemma OAI.ErdosGallai.endpointLoad_sum line 800
  56. def OAI.ErdosGallai.usedEdges line 816
  57. lemma OAI.ErdosGallai.usedEdges_card_le line 819
  58. lemma OAI.ErdosGallai.usedEdges_update_insert line 828
  59. def OAI.ErdosGallai.teamInterior line 841
  60. lemma OAI.ErdosGallai.teamInterior_card_le line 845
  61. structure OAI.ErdosGallai.PartialRoutes line 864
  62. theorem OAI.ErdosGallai.routing line 874