OAI/Computability/BinPacking/Packing/PhaseIteration.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.UniformTree.leafRank line 11
  2. theorem OAI.BinPackingGap.UniformTree.leafRank_pos line 14
  3. theorem OAI.BinPackingGap.UniformTree.one_le_leafRank line 18
  4. theorem OAI.BinPackingGap.UniformTree.leafRank_le line 21
  5. theorem OAI.BinPackingGap.UniformTree.leafRank_injective line 26
  6. theorem OAI.BinPackingGap.UniformTree.leaf_card_pos line 32
  7. def OAI.BinPackingGap.UniformTree.rankedGadget line 35
  8. theorem OAI.BinPackingGap.UniformTree.rankedGadget_height line 39
  9. theorem OAI.BinPackingGap.UniformTree.rankedGadget_quota line 42
  10. theorem OAI.BinPackingGap.UniformTree.rankedGadget_red_depth line 45
  11. theorem OAI.BinPackingGap.UniformTree.rankedGadget_blue_depth line 49
  12. theorem OAI.BinPackingGap.UniformTree.rankedGadget_card_red line 53
  13. theorem OAI.BinPackingGap.UniformTree.rankedGadget_card_blue line 57
  14. def OAI.BinPackingGap.UniformTree.nextPhase line 61
  15. theorem OAI.BinPackingGap.UniformTree.nextPhase_height line 65
  16. theorem OAI.BinPackingGap.UniformTree.height_lt_nextPhase line 68
  17. theorem OAI.BinPackingGap.UniformTree.mem_nextPhase_leaves line 72
  18. def OAI.BinPackingGap.UniformTree.singletonRoot line 77
  19. def OAI.BinPackingGap.AuxiliaryTree.initial line 94
  20. def OAI.BinPackingGap.AuxiliaryTree.step line 122
  21. theorem OAI.BinPackingGap.AuxiliaryTree.step_height line 225
  22. theorem OAI.BinPackingGap.AuxiliaryTree.height_lt_step line 228
  23. def OAI.BinPackingGap.buildAuxiliary line 233
  24. theorem OAI.BinPackingGap.buildAuxiliary_zero line 237
  25. theorem OAI.BinPackingGap.buildAuxiliary_succ line 239
  26. theorem OAI.BinPackingGap.phases_le_buildAuxiliary_height line 242
  27. theorem OAI.BinPackingGap.buildAuxiliary_height_pos line 250