OAI/Computability/BinPacking/Configurations/ConfigurationLP.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.FractionalCover.objective_nonneg line 24
  2. theorem OAI.BinPackingGap.FractionalCover.coordinate_le_objective line 28
  3. theorem OAI.BinPackingGap.FractionalCover.objectiveSet_nonempty line 32
  4. theorem OAI.BinPackingGap.FractionalCover.objectiveSet_bddBelow line 37
  5. theorem OAI.BinPackingGap.FractionalCover.value_le_of_feasible line 43
  6. theorem OAI.BinPackingGap.FractionalCover.le_value_of_lower_bound line 47
  7. theorem OAI.BinPackingGap.FractionalCover.value_nonneg line 54
  8. theorem OAI.BinPackingGap.FractionalCover.continuous_objective line 58
  9. theorem OAI.BinPackingGap.FractionalCover.continuous_coverage line 62
  10. theorem OAI.BinPackingGap.FractionalCover.isClosed_feasible line 66
  11. theorem OAI.BinPackingGap.FractionalCover.isCompact_sublevel line 76
  12. theorem OAI.BinPackingGap.FractionalCover.exists_minimum line 84
  13. theorem OAI.BinPackingGap.FractionalCover.exists_minimizer line 96
  14. theorem OAI.BinPackingGap.FractionalCover.value_eq_of_feasible_of_lower_bound line 103
  15. theorem OAI.BinPackingGap.FractionalCover.sum_demand_le_mul_objective line 110
  16. theorem OAI.BinPackingGap.FractionalCover.sum_demand_le_mul_value line 123
  17. def OAI.BinPackingGap.FractionalCover.pushforward line 132
  18. theorem OAI.BinPackingGap.FractionalCover.pushforward_nonneg line 137
  19. theorem OAI.BinPackingGap.FractionalCover.objective_pushforward line 146
  20. theorem OAI.BinPackingGap.FractionalCover.coverage_pushforward line 153
  21. theorem OAI.BinPackingGap.FractionalCover.feasible_pushforward line 160
  22. theorem OAI.BinPackingGap.NumericalSize.le_one line 180
  23. def OAI.BinPackingGap.NumericalSize.ofItem line 185
  24. theorem OAI.BinPackingGap.NumericalSize.ofItem_val line 188
  25. def OAI.BinPackingGap.TypeConfiguration.empty line 196
  26. instance OAI.BinPackingGap.TypeConfiguration.(instance at line 198) line 198
  27. def OAI.BinPackingGap.TypeConfiguration.ofIndividual line 200
  28. theorem OAI.BinPackingGap.TypeConfiguration.ofIndividual_count line 231
  29. theorem OAI.BinPackingGap.TypeConfiguration.card_le_five line 234
  30. theorem OAI.BinPackingGap.sum_type_multiplicity line 263
  31. def OAI.BinPackingGap.IndividualFeasible line 283
  32. def OAI.BinPackingGap.TypeFeasible line 286
  33. theorem OAI.BinPackingGap.individualMatrix_sum line 289
  34. theorem OAI.BinPackingGap.typeMatrix_sum line 294
  35. def OAI.BinPackingGap.singletonWeights line 298
  36. theorem OAI.BinPackingGap.singletonWeights_feasible line 301
  37. theorem OAI.BinPackingGap.singletonWeights_objective line 310
  38. theorem OAI.BinPackingGap.individualLP_attained line 315
  39. theorem OAI.BinPackingGap.individualLP_nonneg line 319
  40. theorem OAI.BinPackingGap.individualLP_le_n line 322
  41. theorem OAI.BinPackingGap.typeMatrix_ofIndividual line 326
  42. def OAI.BinPackingGap.projectWeights line 344
  43. theorem OAI.BinPackingGap.projectWeights_objective line 348
  44. theorem OAI.BinPackingGap.projectWeights_feasible line 352
  45. theorem OAI.BinPackingGap.typeLP_attained line 378
  46. theorem OAI.BinPackingGap.typeLP_nonneg line 383
  47. theorem OAI.BinPackingGap.typeLP_le_individualLP line 387
  48. theorem OAI.BinPackingGap.individualLP_eq_zero_of_n_eq_zero line 394
  49. theorem OAI.BinPackingGap.typeLP_eq_zero_of_n_eq_zero line 400
  50. def OAI.BinPackingGap.Packing.fractionalWeights line 407
  51. theorem OAI.BinPackingGap.Packing.fractionalWeights_feasible line 411
  52. theorem OAI.BinPackingGap.Packing.fractionalWeights_objective line 421
  53. theorem OAI.BinPackingGap.individualLP_le_opt line 428
  54. theorem OAI.BinPackingGap.typeLP_le_opt line 433
  55. theorem OAI.BinPackingGap.n_le_five_mul_individual_objective line 436
  56. theorem OAI.BinPackingGap.n_le_five_mul_type_objective line 446
  57. theorem OAI.BinPackingGap.n_le_five_mul_individualLP line 459
  58. theorem OAI.BinPackingGap.n_le_five_mul_typeLP line 465
  59. theorem OAI.BinPackingGap.bothLP_eq_of_physical_witness line 471