OAI/Computability/BinPacking/Packing/PrimaryLoss.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.PrimaryLoss.binItems line 17
  2. abbrev OAI.BinPackingGap.PrimaryLoss.fiber line 20
  3. def OAI.BinPackingGap.PrimaryLoss.itemsIn line 22
  4. def OAI.BinPackingGap.PrimaryLoss.binPrimary line 25
  5. def OAI.BinPackingGap.PrimaryLoss.fullBins line 28
  6. def OAI.BinPackingGap.PrimaryLoss.nonfullBins line 31
  7. def OAI.BinPackingGap.PrimaryLoss.nonfullItems line 34
  8. def OAI.BinPackingGap.PrimaryLoss.negativeFullBins line 36
  9. def OAI.BinPackingGap.PrimaryLoss.outsideZeroFullItems line 39
  10. theorem OAI.BinPackingGap.PrimaryLoss.fibers_disjoint line 43
  11. theorem OAI.BinPackingGap.PrimaryLoss.sum_fibers line 50
  12. theorem OAI.BinPackingGap.PrimaryLoss.card_itemsIn line 55
  13. theorem OAI.BinPackingGap.PrimaryLoss.sum_fiber_card line 59
  14. theorem OAI.BinPackingGap.PrimaryLoss.sum_binPrimary line 63
  15. theorem OAI.BinPackingGap.PrimaryLoss.card_itemsIn_le line 67
  16. theorem OAI.BinPackingGap.PrimaryLoss.nonfullBins_card_le line 76
  17. theorem OAI.BinPackingGap.PrimaryLoss.nonfullItems_card_le line 95
  18. theorem OAI.BinPackingGap.PrimaryLoss.full_nonfull_disjoint line 104
  19. theorem OAI.BinPackingGap.PrimaryLoss.full_nonfull_union line 112
  20. theorem OAI.BinPackingGap.PrimaryLoss.primary_conservation line 121
  21. theorem OAI.BinPackingGap.PrimaryLoss.negativeFullBins_card_le line 128
  22. theorem OAI.BinPackingGap.PrimaryLoss.outsideZeroFullItems_eq line 166
  23. theorem OAI.BinPackingGap.PrimaryLoss.loss_items_disjoint line 177
  24. theorem OAI.BinPackingGap.PrimaryLoss.primary_loss_bound line 186