OAI/Computability/BinPacking/Packing/K4Graph.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.primaryScoreBound line 24
  2. def OAI.BinPackingGap.lossAllowance line 26
  3. def OAI.BinPackingGap.depthDemand line 28
  4. def OAI.BinPackingGap.repetitions line 31
  5. theorem OAI.BinPackingGap.primaryScoreBound_pos line 33
  6. theorem OAI.BinPackingGap.lossAllowance_pos line 37
  7. theorem OAI.BinPackingGap.primary_loss_lt_lossAllowance line 41
  8. theorem OAI.BinPackingGap.depthDemand_ge_72_real line 47
  9. theorem OAI.BinPackingGap.depthDemand_ge_72 line 51
  10. theorem OAI.BinPackingGap.depthDemand_ge_120_div line 55
  11. theorem OAI.BinPackingGap.depthDemand_pos line 59
  12. theorem OAI.BinPackingGap.depthDemand_one_le line 63
  13. theorem OAI.BinPackingGap.depthDemand_ge_12 line 66
  14. theorem OAI.BinPackingGap.depthDemand_spec line 71
  15. theorem OAI.BinPackingGap.threshold_gap line 77
  16. theorem OAI.BinPackingGap.three_quarter_lower line 81
  17. theorem OAI.BinPackingGap.depthDemand_threshold_gap line 85
  18. theorem OAI.BinPackingGap.repetitions_pos line 89
  19. theorem OAI.BinPackingGap.repetitions_gt_P line 93
  20. theorem OAI.BinPackingGap.repetitions_cast line 98
  21. theorem OAI.BinPackingGap.edge_demand_exceeds_capacity_real line 102
  22. theorem OAI.BinPackingGap.edge_demand_exceeds_capacity line 113
  23. theorem OAI.BinPackingGap.sixty_loss_div_le line 120
  24. theorem OAI.BinPackingGap.depthDemand_sixty_loss_div_le line 130
  25. structure OAI.BinPackingGap.GraphInput line 135
  26. abbrev OAI.BinPackingGap.GraphInput.Vertex line 143
  27. abbrev OAI.BinPackingGap.GraphInput.Edge line 145
  28. def OAI.BinPackingGap.GraphInput.left line 147
  29. def OAI.BinPackingGap.GraphInput.right line 149
  30. def OAI.BinPackingGap.GraphInput.IsCover line 151
  31. def OAI.BinPackingGap.GraphInput.CoverAtMost line 154
  32. def OAI.BinPackingGap.GraphInput.endpoint line 163
  33. theorem OAI.BinPackingGap.GraphInput.endpoint_zero line 166
  34. theorem OAI.BinPackingGap.GraphInput.endpoint_one line 169
  35. theorem OAI.BinPackingGap.GraphInput.left_lt_right line 172
  36. theorem OAI.BinPackingGap.GraphInput.left_ne_right line 175
  37. theorem OAI.BinPackingGap.GraphInput.endpoint_injective line 178
  38. abbrev OAI.BinPackingGap.GraphInput.Incidence line 189
  39. def OAI.BinPackingGap.GraphInput.incidenceEquiv line 192
  40. def OAI.BinPackingGap.GraphInput.degree line 196
  41. theorem OAI.BinPackingGap.GraphInput.sum_degree line 199
  42. abbrev OAI.BinPackingGap.GraphInput.IncidencePosition line 204
  43. abbrev OAI.BinPackingGap.GraphInput.JobCopy line 207
  44. theorem OAI.BinPackingGap.GraphInput.card_incidencePosition line 210
  45. theorem OAI.BinPackingGap.GraphInput.card_jobCopy line 214
  46. theorem OAI.BinPackingGap.GraphInput.sum_card_jobCopy line 219
  47. def OAI.BinPackingGap.thresholdCover line 237
  48. def OAI.BinPackingGap.largePlus line 241
  49. theorem OAI.BinPackingGap.residual_plus_le line 245
  50. theorem OAI.BinPackingGap.thresholdCover_card_le_fractions line 286
  51. theorem OAI.BinPackingGap.cover_fraction_bound line 344
  52. theorem OAI.BinPackingGap.thresholdCover_card_le line 361
  53. theorem OAI.BinPackingGap.longMatch_sum_lower line 380
  54. theorem OAI.BinPackingGap.thresholdCover_isCover line 391
  55. theorem OAI.BinPackingGap.thresholdCover_card_le_graph line 447
  56. def OAI.BinPackingGap.completeFourGraph line 466
  57. theorem OAI.BinPackingGap.completeFourGraph_edge_pos line 472
  58. theorem OAI.BinPackingGap.completeFourGraph_cover_card line 474
  59. theorem OAI.BinPackingGap.completeFourGraph_cover_three line 505
  60. theorem OAI.BinPackingGap.completeFourGraph_no_small_cover line 512