OAI/Combinatorics/CycleDecomposition/ReservoirCycles.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ErdosGallai.routing_length_upper line 17
  2. lemma OAI.ErdosGallai.eventually_logb_le_power line 41
  3. lemma OAI.ErdosGallai.eventually_constant_le_power line 50
  4. lemma OAI.ErdosGallai.eventually_const_mul_power_le line 54
  5. theorem OAI.ErdosGallai.eventually_routing_length line 62
  6. theorem OAI.ErdosGallai.batch_routing_margin line 95
  7. lemma OAI.ErdosGallai.eventually_reservoir_capacity line 134
  8. theorem OAI.ErdosGallai.residue_routing_margin line 152
  9. def OAI.ErdosGallai.CutExpansionOn line 196
  10. lemma OAI.ErdosGallai.subtype_image_compl line 200
  11. lemma OAI.ErdosGallai.induced_interedges_card line 214
  12. lemma OAI.ErdosGallai.cutExpansion_induce line 239
  13. theorem OAI.ErdosGallai.routing_allow_equal line 256
  14. theorem OAI.ErdosGallai.routing_in_reservoir line 300
  15. theorem OAI.ErdosGallai.uniform_reservoir_routing line 342
  16. theorem OAI.ErdosGallai.occurrence_slots line 384
  17. def OAI.ErdosGallai.endpointOccurrence line 404
  18. theorem OAI.ErdosGallai.endpoint_occurrence_slots line 407
  19. theorem OAI.ErdosGallai.reserved_edges_injective line 442
  20. theorem OAI.ErdosGallai.assigned_representative_load line 467
  21. theorem OAI.ErdosGallai.choose_reservoir_endpoints line 489
  22. theorem OAI.ErdosGallai.uniform_assigned_reservoir_routing line 551
  23. def OAI.ErdosGallai.reservoirReturn line 602
  24. lemma OAI.ErdosGallai.reservoirReturn_isPath line 605
  25. theorem OAI.ErdosGallai.reservoir_path_closure line 621
  26. lemma OAI.ErdosGallai.spoke_sets_pairwise line 656
  27. lemma OAI.ErdosGallai.pairwise_union_three line 666
  28. theorem OAI.ErdosGallai.reservoir_cycle_family line 688
  29. lemma OAI.ErdosGallai.reservoir_edge_ledger line 721