OAI/Combinatorics/CycleDecomposition/ScaleExtraction.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ErdosGallai.Scale.edgeCount_eq_card line 18
  2. def OAI.ErdosGallai.Scale.IsCycleGraph line 26
  3. def OAI.ErdosGallai.Scale.NoLongCycle line 29
  4. lemma OAI.ErdosGallai.Scale.NoLongCycle.mono line 32
  5. lemma OAI.ErdosGallai.Scale.cycle_graph_of_walk line 37
  6. lemma OAI.ErdosGallai.Scale.edgeCount_sdiff_add line 54
  7. lemma OAI.ErdosGallai.Scale.edgeCount_cycle_pos line 64
  8. theorem OAI.ErdosGallai.Scale.remove_long_cycles line 75
  9. lemma OAI.ErdosGallai.Scale.longCycle_power_margin line 119
  10. lemma OAI.ErdosGallai.Scale.longCycle_scale_ready line 147
  11. lemma OAI.ErdosGallai.Scale.external_induce_image line 186
  12. lemma OAI.ErdosGallai.Scale.sparse_neighborhood_from_cycle_exclusion line 211
  13. lemma OAI.ErdosGallai.Scale.splitPotential_scale_bound line 258
  14. lemma OAI.ErdosGallai.Scale.partition_replace_head line 288
  15. theorem OAI.ErdosGallai.Scale.scale_boxes line 297
  16. lemma OAI.ErdosGallai.Scale.edgeCount_sup_le line 349
  17. lemma OAI.ErdosGallai.Scale.crossing_count line 353
  18. lemma OAI.ErdosGallai.Scale.log2_split_budget line 382
  19. lemma OAI.ErdosGallai.Scale.partition_combine line 399
  20. lemma OAI.ErdosGallai.Scale.cut_split_properties line 422
  21. lemma OAI.ErdosGallai.Scale.empty_supported_graph line 438
  22. theorem OAI.ErdosGallai.Scale.cut_extraction line 448
  23. lemma OAI.ErdosGallai.Scale.cast_log2_le_logb line 544
  24. lemma OAI.ErdosGallai.Scale.expansion_order_lower line 549
  25. lemma OAI.ErdosGallai.Scale.cut_scale_ready line 566
  26. theorem OAI.ErdosGallai.Scale.scale_cut_extraction line 585