OAI/Combinatorics/EditApproximation/Binary/BinaryScaleGrid.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Literal dyadic scales and the finite initial-cone center list, with binary rational comparisons and bounded grid enumeration.

  1. theorem OAI.EditApproximation.log_two_add_one_eq_size line 13
  2. theorem OAI.EditApproximation.dyadicScalesWithWork_value line 23
  3. theorem OAI.EditApproximation.dyadicScalesWithWork_cost line 35
  4. theorem OAI.EditApproximation.seedGridSpacingWithWork_value line 51
  5. theorem OAI.EditApproximation.seedGridSpacingWithWork_pos line 71
  6. theorem OAI.EditApproximation.BinaryFraction.initialScaleGuardWithWork_value line 81
  7. theorem OAI.EditApproximation.BinaryFraction.initialCenterGuardWithWork_value line 90
  8. def OAI.EditApproximation.BinaryFraction.initialCentersWithWork line 97
  9. theorem OAI.EditApproximation.BinaryFraction.initialCentersWithWork_value line 108
  10. def OAI.EditApproximation.BinaryFraction.initialProgramWithWork line 127
  11. theorem OAI.EditApproximation.BinaryFraction.initialProgramWithWork_value line 133