OAI/Combinatorics/EditApproximation/Geometry/ParameterConstruction.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Counted register loops for the global integer parameters. Multiplication and division here are word operations; the word-cap theorem below supplies room for their intermediate integers.

  1. theorem OAI.EditApproximation.size_pred_eq_clog_two line 14
  2. theorem OAI.EditApproximation.size_pred_eq_log_two line 21
  3. theorem OAI.EditApproximation.parameterClogWithWork_spec line 33
  4. theorem OAI.EditApproximation.parameterLogWithWork_value line 39
  5. theorem OAI.EditApproximation.parameterLogWithWork_cost line 43
  6. theorem OAI.EditApproximation.parameterRootSearch_value line 49
  7. theorem OAI.EditApproximation.parameterRootSearch_cost line 64
  8. theorem OAI.EditApproximation.parameterSqrtWithWork_value line 74
  9. theorem OAI.EditApproximation.parameterSqrtWithWork_cost line 78
  10. theorem OAI.EditApproximation.parameterPowerWithWork_spec line 83
  11. theorem OAI.EditApproximation.parameterPowerWithWork_intermediate line 89
  12. theorem OAI.EditApproximation.integerParametersWithWork_value line 96
  13. theorem OAI.EditApproximation.integerParametersWithWork_cost line 102
  14. theorem OAI.EditApproximation.integerParameter_power_word_cap line 138
  15. theorem OAI.EditApproximation.parameterPowerWithWork_word_cap line 147
  16. theorem OAI.EditApproximation.parameterRootSearch_word_cap line 152