OAI/Combinatorics/CycleDecomposition/ScaleHierarchy.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ErdosGallai.Scale.edgeOccurrences_refine line 19
  2. lemma OAI.ErdosGallai.Scale.graphPartition_refine line 30
  3. theorem OAI.ErdosGallai.Scale.scale_split line 39
  4. def OAI.ErdosGallai.Scale.scaleTheta line 96
  5. def OAI.ErdosGallai.Scale.inductionScale line 97
  6. lemma OAI.ErdosGallai.Scale.scaleTheta_pos line 99
  7. lemma OAI.ErdosGallai.Scale.scaleTheta_lt_one line 100
  8. lemma OAI.ErdosGallai.Scale.inductionScale_zero line 102
  9. lemma OAI.ErdosGallai.Scale.inductionScale_pos line 105
  10. lemma OAI.ErdosGallai.Scale.inductionScale_succ line 108
  11. lemma OAI.ErdosGallai.Scale.inductionScale_gt_one line 112
  12. lemma OAI.ErdosGallai.Scale.inductionScale_le line 117
  13. lemma OAI.ErdosGallai.Scale.inductionScale_log line 122
  14. lemma OAI.ErdosGallai.Scale.inductionScale_log_pos line 126
  15. lemma OAI.ErdosGallai.Scale.inductionScale_log_succ line 130
  16. lemma OAI.ErdosGallai.Scale.inductionScale_add line 135
  17. lemma OAI.ErdosGallai.Scale.inductionScale_window line 139
  18. lemma OAI.ErdosGallai.Scale.inductionScale_tendsto line 143
  19. theorem OAI.ErdosGallai.Scale.inductionScale_first_cutoff line 150
  20. theorem OAI.ErdosGallai.Scale.scale_reciprocal_log_sum line 166
  21. lemma OAI.ErdosGallai.Scale.exp_le_one_add_twice line 186
  22. theorem OAI.ErdosGallai.Scale.scale_overlap_product line 192
  23. theorem OAI.ErdosGallai.Scale.scale_prefix_cycle_cost line 221
  24. structure OAI.ErdosGallai.Scale.StageSplit line 255
  25. def OAI.ErdosGallai.Scale.StageSplit.Bounded line 270
  26. def OAI.ErdosGallai.Scale.StageSplit.trivial line 279
  27. theorem OAI.ErdosGallai.Scale.scale_splitter line 294
  28. def OAI.ErdosGallai.Scale.StageSplit.children line 329
  29. lemma OAI.ErdosGallai.Scale.StageSplit.mem_children line 332
  30. lemma OAI.ErdosGallai.Scale.StageSplit.children_map line 341
  31. lemma OAI.ErdosGallai.Scale.list_disjoint_card_le line 350
  32. def OAI.ErdosGallai.Scale.vertexMass line 368
  33. lemma OAI.ErdosGallai.Scale.vertexMass_nonneg line 371
  34. lemma OAI.ErdosGallai.Scale.vertexMass_nil line 374
  35. lemma OAI.ErdosGallai.Scale.vertexMass_cons line 375
  36. lemma OAI.ErdosGallai.Scale.vertexMass_append line 377
  37. lemma OAI.ErdosGallai.Scale.vertexMass_flatMap line 379
  38. lemma OAI.ErdosGallai.Scale.StageSplit.children_mass line 385
  39. lemma OAI.ErdosGallai.Scale.StageSplit.pieces_mass line 390
  40. abbrev OAI.ErdosGallai.Scale.SplitSystem line 407
  41. def OAI.ErdosGallai.Scale.nextLayer line 410
  42. def OAI.ErdosGallai.Scale.advance line 413
  43. lemma OAI.ErdosGallai.Scale.advance_zero line 417
  44. lemma OAI.ErdosGallai.Scale.advance_succ line 418
  45. lemma OAI.ErdosGallai.Scale.advance_add line 421
  46. lemma OAI.ErdosGallai.Scale.advance_flatMap line 427
  47. lemma OAI.ErdosGallai.Scale.nextLayer_mem line 434
  48. lemma OAI.ErdosGallai.Scale.advance_subset line 439
  49. lemma OAI.ErdosGallai.Scale.advance_nonempty line 450
  50. lemma OAI.ErdosGallai.Scale.advance_cover line 461
  51. lemma OAI.ErdosGallai.Scale.list_union_mem line 472
  52. lemma OAI.ErdosGallai.Scale.list_union_card line 480
  53. lemma OAI.ErdosGallai.Scale.list_cover_card_le line 491
  54. lemma OAI.ErdosGallai.Scale.advance_mass_lower line 497
  55. lemma OAI.ErdosGallai.Scale.nextLayer_mass_bound line 501
  56. lemma OAI.ErdosGallai.Scale.advance_valid line 514
  57. lemma OAI.ErdosGallai.Scale.advance_bounded line 535
  58. lemma OAI.ErdosGallai.Scale.advance_mass_global_product line 548