OAI/Combinatorics/EditApproximation/Binary/BinaryLogWork.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Bit cost of the finite logarithm series on unreduced Boolean fractions. Every bound is for the executed power/division/addition loops.

  1. def OAI.EditApproximation.BinaryFraction.logarithmPartialWordBudget line 11
  2. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialWordBudget_input line 18
  3. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialWordBudget_power line 23
  4. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialWordBudget_partial line 31
  5. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialWordBudget_nat line 40
  6. theorem OAI.EditApproximation.BinaryFraction.divWithWork_self_width line 48
  7. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialWordBudget_term line 52
  8. def OAI.EditApproximation.BinaryFraction.logarithmPartialBitStep line 68
  9. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialWithWork_cost_le line 72
  10. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialWithWork_cost line 108
  11. theorem OAI.EditApproximation.BinaryFraction.logarithmRatio_abs_le_one line 113
  12. def OAI.EditApproximation.BinaryFraction.logarithmUniversalWordBudget line 123
  13. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialWordBudget_le line 127
  14. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialBitStep_mono line 135
  15. def OAI.EditApproximation.BinaryFraction.logarithmRatio line 145
  16. theorem OAI.EditApproximation.BinaryFraction.logarithmRatio_width line 148
  17. theorem OAI.EditApproximation.BinaryFraction.one_width line 157
  18. theorem OAI.EditApproximation.BinaryFraction.sub_one_width line 159
  19. theorem OAI.EditApproximation.BinaryFraction.add_one_width line 168
  20. def OAI.EditApproximation.BinaryFraction.logarithmBitBudget line 176
  21. theorem OAI.EditApproximation.BinaryFraction.logarithmWithWork_cost line 181
  22. def OAI.EditApproximation.BinaryFraction.generalPowerWordBudget line 207
  23. theorem OAI.EditApproximation.BinaryFraction.powWithWork_cost_general line 210
  24. theorem OAI.EditApproximation.BinaryFraction.logarithmUniversalWordBudget_mono line 224
  25. theorem OAI.EditApproximation.BinaryFraction.logarithmBitBudget_mono line 231