OAI/Combinatorics/EditApproximation/Binary/BinaryPowerStorage.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Construction of a prescribed power denominator uses literal Boolean multiplication and trimming. The subsequent cache compression therefore has no uncharged conversion from a natural number to its binary representation.

  1. theorem OAI.EditApproximation.bitPowerWithWork_value line 15
  2. theorem OAI.EditApproximation.bitPowerWithWork_length line 22
  3. theorem OAI.EditApproximation.bitPowerWithWork_length_le line 30
  4. def OAI.EditApproximation.bitPowerBitBudget line 37
  5. theorem OAI.EditApproximation.bitPowerWithWork_cost line 40
  6. theorem OAI.EditApproximation.refinementBaseWithWork_value line 79
  7. theorem OAI.EditApproximation.refinementBaseWithWork_length line 84
  8. theorem OAI.EditApproximation.refinementBaseWithWork_length_le line 89
  9. theorem OAI.EditApproximation.refinementBaseWithWork_cost line 98
  10. theorem OAI.EditApproximation.BinaryFraction.powerDenominatorWithWork_value line 116
  11. theorem OAI.EditApproximation.BinaryFraction.powerDenominatorWithWork_width line 122
  12. def OAI.EditApproximation.BinaryFraction.powerDenominatorBitBudget line 131
  13. theorem OAI.EditApproximation.BinaryFraction.powerDenominatorWithWork_cost line 134