OAI/Combinatorics/EditApproximation/Binary/BinaryLocalGridWork.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Binary work for the actual bounded endpoint-index loops. The bound is linear in the emitted one-dimensional grid size and quadratic in bit width.

  1. theorem OAI.EditApproximation.wordValue_size_le line 10
  2. theorem OAI.EditApproximation.binaryNaturalAdd_size_le line 13
  3. def OAI.EditApproximation.gridPointsBitBudget line 22
  4. theorem OAI.EditApproximation.gridPointsWithWork_cost line 25
  5. theorem OAI.EditApproximation.makeStateWithWork_cost line 98
  6. def OAI.EditApproximation.gridStateBoxBitBudget line 108
  7. theorem OAI.EditApproximation.gridStateBoxWithWork_cost line 112