OAI/Computability/BinPacking/Packing/FractionWidth.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.Instance.ofFintype line 24
  2. def OAI.BinPackingGap.Packing.binItems line 37
  3. theorem OAI.BinPackingGap.Packing.mem_binItems line 40
  4. theorem OAI.BinPackingGap.Packing.bin_capacity line 44
  5. theorem OAI.BinPackingGap.Packing.binItems_disjoint line 48
  6. theorem OAI.BinPackingGap.Packing.mem_own_bin line 56
  7. theorem OAI.BinPackingGap.Packing.unique_bin line 59
  8. theorem OAI.BinPackingGap.Packing.chosen_injective line 65
  9. theorem OAI.BinPackingGap.Packing.sum_bins line 76
  10. theorem OAI.BinPackingGap.Packing.sum_bin_card line 91
  11. def OAI.BinPackingGap.Packing.enlarge line 95
  12. theorem OAI.BinPackingGap.opt_attained line 113
  13. theorem OAI.BinPackingGap.opt_le_of_hasPacking line 117
  14. theorem OAI.BinPackingGap.opt_le_n line 122
  15. theorem OAI.BinPackingGap.opt_eq_zero_of_n_eq_zero line 125
  16. theorem OAI.BinPackingGap.HasPacking.mono line 129
  17. theorem OAI.BinPackingGap.hasPacking_iff_opt_le line 134
  18. theorem OAI.BinPackingGap.not_hasPacking_iff_lt_opt line 138
  19. def OAI.BinPackingGap.packingOfFintype line 142
  20. def OAI.BinPackingGap.IndividualConfiguration.singleton line 160
  21. theorem OAI.BinPackingGap.IndividualConfiguration.card_le_five line 163
  22. def OAI.BinPackingGap.Packing.configuration line 179
  23. theorem OAI.BinPackingGap.Packing.bin_card_le_five line 182
  24. theorem OAI.BinPackingGap.Packing.item_count_le_five_mul line 187
  25. structure OAI.BinPackingGap.Instance.Reindexing line 199
  26. def OAI.BinPackingGap.Instance.Reindexing.symm line 207
  27. theorem OAI.BinPackingGap.Instance.Reindexing.count_eq line 212
  28. theorem OAI.BinPackingGap.Instance.Reindexing.lower_bound_iff line 215
  29. def OAI.BinPackingGap.Packing.reindex line 230
  30. theorem OAI.BinPackingGap.Instance.Reindexing.hasPacking_iff line 252
  31. theorem OAI.BinPackingGap.Instance.Reindexing.opt_eq line 260
  32. theorem OAI.BinPackingGap.RawInstance.toInstance_n line 269
  33. theorem OAI.BinPackingGap.RawInstance.toInstance_size line 272
  34. theorem OAI.BinPackingGap.RawInstance.valid_nil line 275
  35. def OAI.BinPackingGap.RawPacking.addFraction line 281
  36. def OAI.BinPackingGap.RawPacking.loadFraction line 284
  37. theorem OAI.BinPackingGap.RawPacking.addFraction_den_pos line 288
  38. theorem OAI.BinPackingGap.RawPacking.ratValue_addFraction line 291
  39. theorem OAI.BinPackingGap.RawPacking.foldFraction_spec line 300
  40. theorem OAI.BinPackingGap.RawPacking.zip_den_pos line 325
  41. theorem OAI.BinPackingGap.RawPacking.loadFraction_den_pos line 330
  42. theorem OAI.BinPackingGap.RawPacking.load_eq_loadFraction line 334
  43. theorem OAI.BinPackingGap.RawPacking.load_le_one_iff line 339
  44. theorem OAI.BinPackingGap.RawPacking.load_eq_zero_of_not_mem line 346
  45. theorem OAI.BinPackingGap.RawPacking.feasible_iff_mem_capacity line 356
  46. theorem OAI.BinPackingGap.RawPacking.zip_ofFn_eq line 371
  47. theorem OAI.BinPackingGap.RawPacking.load_ofFn line 377
  48. def OAI.BinPackingGap.RawPacking.assignmentFn line 387
  49. theorem OAI.BinPackingGap.RawPacking.assignments_eq_ofFn line 391
  50. def OAI.BinPackingGap.RawPacking.toPacking line 397
  51. theorem OAI.BinPackingGap.RawPacking.toPacking_assignment_val line 406
  52. def OAI.BinPackingGap.RawPacking.ofPacking line 410
  53. theorem OAI.BinPackingGap.RawPacking.ofPacking_feasible line 414
  54. theorem OAI.BinPackingGap.RawPacking.feasible_iff_exists_packing line 426
  55. theorem OAI.BinPackingGap.RawPacking.hasPacking_iff_exists_feasible line 437
  56. theorem OAI.BinPackingGap.RawPacking.feasible_nil_iff line 446
  57. theorem OAI.BinPackingGap.RawPacking.feasible_zero_bins_iff line 458
  58. def OAI.BinPackingGap.Instance.toRaw line 476
  59. theorem OAI.BinPackingGap.Instance.toRaw_length line 479
  60. theorem OAI.BinPackingGap.Instance.ratValue_num_den line 482
  61. theorem OAI.BinPackingGap.Instance.toRaw_valid line 489
  62. theorem OAI.BinPackingGap.Instance.toRaw_size line 500
  63. def OAI.BinPackingGap.Instance.toRawReindexing line 509
  64. theorem OAI.BinPackingGap.Instance.eq_of_indexed_sizes line 518
  65. theorem OAI.BinPackingGap.Instance.toInstance_toRaw line 531
  66. theorem OAI.BinPackingGap.RawPacking.ofPacking_cast line 541
  67. theorem OAI.BinPackingGap.RawPacking.ofPacking_toRaw_feasible line 546
  68. def OAI.BinPackingGap.FractionWidth.denominatorBits line 558
  69. theorem OAI.BinPackingGap.FractionWidth.denominatorBits_nil line 561
  70. theorem OAI.BinPackingGap.FractionWidth.denominatorBits_cons line 563
  71. theorem OAI.BinPackingGap.FractionWidth.size_mono line 566
  72. theorem OAI.BinPackingGap.FractionWidth.size_mul_le line 570
  73. theorem OAI.BinPackingGap.FractionWidth.size_add_le line 580
  74. theorem OAI.BinPackingGap.FractionWidth.addFraction_left_product_size_le line 586
  75. theorem OAI.BinPackingGap.FractionWidth.addFraction_right_product_size_le line 590
  76. theorem OAI.BinPackingGap.FractionWidth.addFraction_num_size_le line 596
  77. theorem OAI.BinPackingGap.FractionWidth.addFraction_den_size_le line 602
  78. theorem OAI.BinPackingGap.FractionWidth.fold_den_size_le line 606
  79. theorem OAI.BinPackingGap.FractionWidth.loadFraction_den_size_le line 626
  80. theorem OAI.BinPackingGap.FractionWidth.loadFraction_num_size_le_of_accepted line 631
  81. theorem OAI.BinPackingGap.FractionWidth.addFraction_width_of_budget line 637
  82. theorem OAI.BinPackingGap.FractionWidth.loadFraction_next_width line 649
  83. theorem OAI.BinPackingGap.FractionWidth.addFraction_overflow line 663
  84. theorem OAI.BinPackingGap.FractionWidth.fold_overflow line 669