OAI/Combinatorics/EditApproximation/Geometry/LocalArithmeticAsymptotics.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual finite optimizer arithmetic counter is subpolynomial in the input length. This statement does not include the separate bit-operation and local-data preparation counters.

  1. def OAI.EditApproximation.computedLocalArithmeticExponent line 16
  2. theorem OAI.EditApproximation.computedLocalArithmeticExponent_tendsto line 21
  3. theorem OAI.EditApproximation.computedLocalOptimizer_arithmetic_exp_bound line 34
  4. theorem OAI.EditApproximation.computedLocalOptimizer_arithmetic_subpolynomial line 68