OAI/Computability/BinPacking/Machines/IntegerPackingArithmetic.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.IntegerPackingArithmetic.widthRadix line 8
  2. def OAI.BinPackingGap.IntegerPackingArithmetic.geomDenominator line 10
  3. def OAI.BinPackingGap.IntegerPackingArithmetic.sizeDenominator line 13
  4. def OAI.BinPackingGap.IntegerPackingArithmetic.signedNumerator line 16
  5. def OAI.BinPackingGap.IntegerPackingArithmetic.itemNumerator line 20
  6. theorem OAI.BinPackingGap.IntegerPackingArithmetic.widthRadix_pos line 24
  7. theorem OAI.BinPackingGap.IntegerPackingArithmetic.geomDenominator_pos line 28
  8. theorem OAI.BinPackingGap.IntegerPackingArithmetic.sizeDenominator_pos line 32
  9. theorem OAI.BinPackingGap.IntegerPackingArithmetic.signedNumerator_ratio line 37
  10. theorem OAI.BinPackingGap.IntegerPackingArithmetic.itemNumerator_ratio line 50
  11. theorem OAI.BinPackingGap.IntegerPackingArithmetic.itemNumerator_pos_lt line 56
  12. def OAI.BinPackingGap.IntegerPackingArithmetic.rawItem line 78
  13. theorem OAI.BinPackingGap.IntegerPackingArithmetic.rawItem_numerator_cast line 82
  14. theorem OAI.BinPackingGap.IntegerPackingArithmetic.rawItem_valid line 88
  15. theorem OAI.BinPackingGap.IntegerPackingArithmetic.rawItem_ratio line 97
  16. def OAI.BinPackingGap.IntegerPackingArithmetic.localNumerator line 108
  17. theorem OAI.BinPackingGap.IntegerPackingArithmetic.geomDenominator_mul_gap line 110
  18. theorem OAI.BinPackingGap.IntegerPackingArithmetic.geomDenominator_mul_lambda line 120
  19. theorem OAI.BinPackingGap.IntegerPackingArithmetic.geomDenominator_mul_delta line 134
  20. def OAI.BinPackingGap.IntegerPackingArithmetic.baselineNumerator line 139
  21. def OAI.BinPackingGap.IntegerPackingArithmetic.betaNumerator line 144
  22. theorem OAI.BinPackingGap.IntegerPackingArithmetic.geomDenominator_mul_baseline line 147
  23. theorem OAI.BinPackingGap.IntegerPackingArithmetic.geomDenominator_mul_beta line 155