OAI/Combinatorics/EditApproximation/Binary/BinaryInitialMinimumWork.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The initial entry's complete arithmetic counter, including its zero test, spatial coefficient, fallback and finite minimum. Grid construction is charged by the separate local endpoint enumerator.

  1. def OAI.EditApproximation.BinaryFraction.initialMinimumInputBudget line 12
  2. def OAI.EditApproximation.BinaryFraction.initialMinimumWordBudget line 14
  3. def OAI.EditApproximation.BinaryFraction.initialMinimumBitBudget line 17
  4. theorem OAI.EditApproximation.BinaryFraction.initialMinimumWithWork_bounds line 22