OAI/Combinatorics/CycleDecomposition/BatchRouting.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ErdosGallai.Batch.family_quotient_image_order line 16
  2. lemma OAI.ErdosGallai.Batch.PreparedBatch.quotient_supported line 46
  3. def OAI.ErdosGallai.Batch.CutExpansion line 77
  4. lemma OAI.ErdosGallai.Batch.boundary_sym2_injective line 81
  5. lemma OAI.ErdosGallai.Batch.deleted_boundary_card_le line 92
  6. theorem OAI.ErdosGallai.Batch.routing_union_growth_step_of_boundary line 102
  7. theorem OAI.ErdosGallai.Batch.routing_union_growth_step line 181
  8. def OAI.ErdosGallai.Batch.avoidGraph line 202
  9. def OAI.ErdosGallai.Batch.walkBall line 210
  10. lemma OAI.ErdosGallai.Batch.mem_walkBall line 214
  11. lemma OAI.ErdosGallai.Batch.root_mem_walkBall line 219
  12. lemma OAI.ErdosGallai.Batch.walkBall_mono line 223
  13. lemma OAI.ErdosGallai.Batch.walk_avoids_end line 229
  14. lemma OAI.ErdosGallai.Batch.ball_avoids line 235
  15. lemma OAI.ErdosGallai.Batch.walkBall_step line 242
  16. def OAI.ErdosGallai.Batch.rootBallUnion line 249
  17. lemma OAI.ErdosGallai.Batch.rootBallUnion_mono_time line 253
  18. lemma OAI.ErdosGallai.Batch.roots_subset_rootBallUnion line 258
  19. theorem OAI.ErdosGallai.Batch.rootBallUnion_growth_step line 263
  20. theorem OAI.ErdosGallai.Batch.rootBallUnion_growth_block line 294
  21. lemma OAI.ErdosGallai.Batch.rootBallUnion_halve line 338
  22. theorem OAI.ErdosGallai.Batch.rootBallUnion_extract_root line 363
  23. lemma OAI.ErdosGallai.Batch.CutExpansion.le_order line 409
  24. def OAI.ErdosGallai.Batch.routingG line 424
  25. def OAI.ErdosGallai.Batch.routingDepth line 426
  26. def OAI.ErdosGallai.Batch.routingLength line 428
  27. lemma OAI.ErdosGallai.Batch.routingG_growth line 430
  28. lemma OAI.ErdosGallai.Batch.le_two_pow_routingDepth line 477
  29. theorem OAI.ErdosGallai.Batch.routing_large_root_ball line 485
  30. def OAI.ErdosGallai.Batch.incidentEdges line 519
  31. lemma OAI.ErdosGallai.Batch.incidentEdges_union line 522
  32. lemma OAI.ErdosGallai.Batch.incidentEdges_union_card_le line 526
  33. lemma OAI.ErdosGallai.Batch.incidentEdges_sum_le line 531
  34. lemma OAI.ErdosGallai.Batch.incidentEdges_path_start_le_one line 546
  35. lemma OAI.ErdosGallai.Batch.incidentEdges_path_end_le_one line 558
  36. lemma OAI.ErdosGallai.Batch.incidentEdges_walk_eq_empty_of_not_mem line 563
  37. lemma OAI.ErdosGallai.Batch.incidentEdges_path_le_two line 571
  38. lemma OAI.ErdosGallai.Batch.deleted_boundary_card_le_incidents line 585
  39. lemma OAI.ErdosGallai.Batch.walkBall_growth_of_incidents line 606
  40. lemma OAI.ErdosGallai.Batch.walkBall_large_of_incidents line 627
  41. lemma OAI.ErdosGallai.Batch.exists_short_avoiding_path line 663
  42. lemma OAI.ErdosGallai.Batch.two_routingG_le_length line 693
  43. lemma OAI.ErdosGallai.Batch.routingLength_bounds line 697
  44. lemma OAI.ErdosGallai.Batch.routing_budget line 720
  45. def OAI.ErdosGallai.Batch.saturated line 745
  46. lemma OAI.ErdosGallai.Batch.saturated_card_le line 749
  47. def OAI.ErdosGallai.Batch.pathInterior line 761
  48. lemma OAI.ErdosGallai.Batch.pathInterior_card_le line 764
  49. lemma OAI.ErdosGallai.Batch.avoidGraph_le line 774
  50. lemma OAI.ErdosGallai.Batch.walk_avoids_support line 777
  51. lemma OAI.ErdosGallai.Batch.walk_avoids_edges line 784
  52. lemma OAI.ErdosGallai.Batch.exists_short_path_with_avoidance line 792
  53. lemma OAI.ErdosGallai.Batch.route_degree_update line 805
  54. def OAI.ErdosGallai.Batch.endpointLoad line 843
  55. lemma OAI.ErdosGallai.Batch.endpointLoad_mono line 846
  56. lemma OAI.ErdosGallai.Batch.endpointLoad_insert line 850
  57. lemma OAI.ErdosGallai.Batch.endpointLoad_sum line 860
  58. def OAI.ErdosGallai.Batch.usedEdges line 876
  59. lemma OAI.ErdosGallai.Batch.usedEdges_card_le line 879
  60. lemma OAI.ErdosGallai.Batch.usedEdges_update_insert line 888
  61. def OAI.ErdosGallai.Batch.teamInterior line 901
  62. lemma OAI.ErdosGallai.Batch.teamInterior_card_le line 905
  63. structure OAI.ErdosGallai.Batch.PartialRoutes line 924
  64. theorem OAI.ErdosGallai.Batch.routing line 934