OAI/Combinatorics/CycleDecomposition/CostRegrouping.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ErdosGallai.Scale.StageSplit.rest line 20
  2. lemma OAI.ErdosGallai.Scale.StageSplit.rest_vertices line 23
  3. lemma OAI.ErdosGallai.Scale.StageSplit.rest_graph line 25
  4. lemma OAI.ErdosGallai.Scale.StageSplit.children_eq_map_rest line 27
  5. lemma OAI.ErdosGallai.Scale.pastPieces_flatMap line 35
  6. lemma OAI.ErdosGallai.Scale.pastCycles_flatMap line 44
  7. lemma OAI.ErdosGallai.Scale.pastPieces_add line 54
  8. lemma OAI.ErdosGallai.Scale.pastCycles_add line 59
  9. lemma OAI.ErdosGallai.Scale.advance_mem_mono line 65
  10. lemma OAI.ErdosGallai.Scale.advance_local_mem line 74
  11. lemma OAI.ErdosGallai.Scale.box_regroup line 87
  12. lemma OAI.ErdosGallai.Scale.piece_list_cost line 112
  13. lemma OAI.ErdosGallai.Scale.box_cost_regroup line 123
  14. def OAI.ErdosGallai.mainP line 149
  15. def OAI.ErdosGallai.mainEta line 150
  16. def OAI.ErdosGallai.mainH line 151
  17. def OAI.ErdosGallai.mainA₁ line 152
  18. def OAI.ErdosGallai.mainA₂ line 153
  19. lemma OAI.ErdosGallai.mainP_pos line 154
  20. lemma OAI.ErdosGallai.mainEta_pos line 155
  21. lemma OAI.ErdosGallai.mainH_pos line 156
  22. lemma OAI.ErdosGallai.mainA₁_nonneg line 157
  23. lemma OAI.ErdosGallai.mainA₂_nonneg line 158
  24. lemma OAI.ErdosGallai.mainEta_mul_P line 159
  25. lemma OAI.ErdosGallai.mainP_eq line 160
  26. structure OAI.ErdosGallai.MainScaleReady line 162
  27. lemma OAI.ErdosGallai.eventually_inverse_power_log line 171
  28. lemma OAI.ErdosGallai.main_scale_ready_cutoff line 184
  29. lemma OAI.ErdosGallai.MainScaleReady.active_square line 203
  30. lemma OAI.ErdosGallai.MainScaleReady.bad_count line 209
  31. lemma OAI.ErdosGallai.MainScaleReady.skip_count line 223
  32. def OAI.ErdosGallai.Scale.costMass line 261
  33. lemma OAI.ErdosGallai.Scale.costMass_bound line 263
  34. lemma OAI.ErdosGallai.Scale.past_cost line 267
  35. lemma OAI.ErdosGallai.Scale.stage_cost line 278
  36. lemma OAI.ErdosGallai.Scale.vertexMass_perm line 286
  37. lemma OAI.ErdosGallai.Scale.pastCycles_sum line 289
  38. lemma OAI.ErdosGallai.Scale.pastPieces_sum line 296
  39. lemma OAI.ErdosGallai.Scale.advance_sum line 301
  40. lemma OAI.ErdosGallai.Scale.pastCycles_after_first line 306
  41. lemma OAI.ErdosGallai.Scale.pastPieces_after_first line 316
  42. lemma OAI.ErdosGallai.Scale.advance_after_first line 326
  43. lemma OAI.ErdosGallai.Scale.selected_input_cost line 333
  44. lemma OAI.ErdosGallai.Scale.selected_prefix_cost line 357