OAI/Combinatorics/EditApproximation/Binary/BinaryOnlineInputWork.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The finite optimistic-history builder uses only the charged Boolean fraction instructions. These bounds derive every intermediate width from the stored table and mass widths.

  1. def OAI.EditApproximation.BinaryFraction.gainBitBudget line 13
  2. theorem OAI.EditApproximation.BinaryFraction.gainWithWork_cost line 15
  3. def OAI.EditApproximation.BinaryFraction.decrementBitBudget line 23
  4. theorem OAI.EditApproximation.BinaryFraction.decrementWithWork_cost line 26
  5. def OAI.EditApproximation.BinaryFraction.coefficientBitBudget line 47
  6. theorem OAI.EditApproximation.BinaryFraction.coefficientWithWork_cost line 50
  7. def OAI.EditApproximation.BinaryFraction.optimisticTermWordBudget line 70
  8. def OAI.EditApproximation.BinaryFraction.optimisticTermBitBudget line 72
  9. theorem OAI.EditApproximation.BinaryFraction.optimisticTermWithWork_cost line 77
  10. def OAI.EditApproximation.BinaryFraction.onlineFinalWordBudget line 116
  11. def OAI.EditApproximation.BinaryFraction.onlineLinearBitBudget line 120
  12. theorem OAI.EditApproximation.BinaryFraction.onlineLinearWithWork_cost line 126