OAI/Combinatorics/EditApproximation/Geometry/Parameters.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Integer-computed parameters

The logarithms and fourth roots in Section 2 are computed by natural bit lengths and nested integer square roots. No real arithmetic oracle is used to form the algorithm's parameters.

  1. theorem OAI.EditApproximation.heightExponent_pos line 33
  2. theorem OAI.EditApproximation.inputHeight_covers_length line 39
  3. theorem OAI.EditApproximation.inputSmallLog_bounds line 44
  4. theorem OAI.EditApproximation.inputHeight_binary_slack line 51
  5. theorem OAI.EditApproximation.inputHeight_polynomial_slack line 58
  6. theorem OAI.EditApproximation.coarseExponent_fourth_power line 63
  7. theorem OAI.EditApproximation.coarseExponent_maximal line 71
  8. theorem OAI.EditApproximation.coarseExponent_shift_square line 77
  9. def OAI.EditApproximation.heightQuarterRoot line 90
  10. theorem OAI.EditApproximation.heightQuarterRoot_fourth_power line 93
  11. theorem OAI.EditApproximation.inputParameters_error_envelope line 100