OAI/Combinatorics/EditApproximation/Binary/BinaryRoundedWork.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Boolean work for the actual canonical rounding and wide-membership tests. Interval endpoints retain their original target bound after rounding.

  1. theorem OAI.EditApproximation.actionEqualWithWork_cost line 10
  2. theorem OAI.EditApproximation.actionMemberWithWork_cost line 29
  3. theorem OAI.EditApproximation.roundStateWithWork_cost line 40
  4. def OAI.EditApproximation.BinaryFraction.roundedSpacingWordBudget line 51
  5. def OAI.EditApproximation.BinaryFraction.roundedSpacingBitBudget line 53
  6. theorem OAI.EditApproximation.BinaryFraction.roundedSpacingWithWork_bounds line 56
  7. def OAI.EditApproximation.BinaryFraction.roundedBandInputBudget line 82
  8. def OAI.EditApproximation.BinaryFraction.roundedBandBitBudget line 85
  9. theorem OAI.EditApproximation.BinaryFraction.roundedBandWithWork_cost line 90