OAI/Combinatorics/EditApproximation/Binary/BinaryOnlineInputs.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The actual optimistic linear objective constructed from stored Boolean fractions, using counted sums, products and divisions. No reduced-rational conversion is used between the table inputs and the optimizer.

  1. theorem OAI.EditApproximation.BinaryFraction.canonicalAddWithWork_value line 17
  2. theorem OAI.EditApproximation.BinaryFraction.canonicalMulWithWork_value line 22
  3. theorem OAI.EditApproximation.BinaryFraction.divWithWork_value line 27
  4. theorem OAI.EditApproximation.BinaryFraction.subWithWork_value line 32
  5. def OAI.EditApproximation.BinaryFraction.gainWithWork line 37
  6. def OAI.EditApproximation.BinaryFraction.decrementWithWork line 42
  7. def OAI.EditApproximation.BinaryFraction.optimisticTermWithWork line 50
  8. theorem OAI.EditApproximation.BinaryFraction.gainWithWork_value line 59
  9. theorem OAI.EditApproximation.BinaryFraction.decrementWithWork_value line 65
  10. theorem OAI.EditApproximation.BinaryFraction.coefficientWithWork_value line 71
  11. def OAI.EditApproximation.BinaryFraction.onlineLinearWithWork line 78
  12. theorem OAI.EditApproximation.BinaryFraction.onlineLinearWithWork_value line 89
  13. theorem OAI.EditApproximation.BinaryFraction.gainWithWork_storage line 105
  14. theorem OAI.EditApproximation.BinaryFraction.decrementWithWork_storage line 117
  15. theorem OAI.EditApproximation.BinaryFraction.coefficientWithWork_storage line 130
  16. def OAI.EditApproximation.BinaryFraction.optimisticTermStorageBudget line 143
  17. theorem OAI.EditApproximation.BinaryFraction.optimisticTermWithWork_storage line 145
  18. def OAI.EditApproximation.BinaryFraction.onlineLinearStorageBudget line 165
  19. theorem OAI.EditApproximation.BinaryFraction.onlineLinearWithWork_storage line 169