OAI/Combinatorics/EditApproximation/Geometry/Grid.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Integer endpoint grids

Rounding is an executable integer division. It preserves valid interval states and shared endpoints, and the edit-distance perturbation is bounded by the actual two remainders. No real-valued grid is substituted for it.

  1. theorem OAI.EditApproximation.gridRound_le line 19
  2. theorem OAI.EditApproximation.gridRound_mono line 22
  3. theorem OAI.EditApproximation.gridRound_distance line 26
  4. theorem OAI.EditApproximation.gridRound_error_lt line 32
  5. theorem OAI.EditApproximation.gridRound_of_dvd line 37
  6. theorem OAI.EditApproximation.gridRound_one line 43
  7. theorem OAI.EditApproximation.roundInterval_shared line 48
  8. theorem OAI.EditApproximation.roundInterval_error line 53
  9. theorem OAI.EditApproximation.edit_roundInterval_bound line 63