OAI/Combinatorics/EditApproximation/Geometry/LocalArithmeticBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The compiled optimizer counter specialized to the literal representative bands. Preparation of the input arrays remains a separate finite loop.

  1. theorem OAI.EditApproximation.computedBandActions_length_le line 11
  2. theorem OAI.EditApproximation.representativeBandActions_length_le line 19
  3. def OAI.EditApproximation.localOptimizerArithmeticBudget line 27
  4. theorem OAI.EditApproximation.materializedRepresentativeBand_work_le line 31
  5. theorem OAI.EditApproximation.localOptimizerArithmeticBudget_cap line 58