OAI/Combinatorics/EditApproximation/Refinement/ComputedOptimizerBitWork.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Substitution of the actual grid and optimizer parameters into the Boolean-operation envelope. Input word bounds remain explicit here so the local rational-value invariants can supply them without a unit-cost rational arithmetic assumption.

  1. def OAI.EditApproximation.localBooleanBitExponent line 16
  2. theorem OAI.EditApproximation.optimizerBitBudget_grid_cap line 19
  3. def OAI.EditApproximation.computedBooleanBitExponent line 62
  4. theorem OAI.EditApproximation.computedBooleanBitExponent_tendsto line 69
  5. def OAI.EditApproximation.computedBooleanBitBudget line 80
  6. theorem OAI.EditApproximation.booleanBitBudget_exp_scalar line 84
  7. theorem OAI.EditApproximation.computedBooleanBitBudget_exp_bound line 99
  8. theorem OAI.EditApproximation.computedBooleanBitBudget_subpolynomial line 111
  9. theorem OAI.EditApproximation.computedBooleanBitBudget_widthWork_near_linear line 117