OAI/Combinatorics/EditApproximation/Geometry/ComparisonBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual terminal, nonterminal-cost and endpoint-movement bounds.

  1. def OAI.EditApproximation.comparisonActiveCost line 11
  2. def OAI.EditApproximation.comparisonMovement line 19
  3. theorem OAI.EditApproximation.comparisonActiveCost_bounds line 28
  4. theorem OAI.EditApproximation.comparisonMovement_bound line 43
  5. theorem OAI.EditApproximation.comparison_total_active_cost_bound line 68
  6. theorem OAI.EditApproximation.comparison_total_movement_bound line 84
  7. theorem OAI.EditApproximation.comparisonStep_stopped_or_width line 102
  8. theorem OAI.EditApproximation.comparison_frontier_stopped_or_width line 131
  9. theorem OAI.EditApproximation.comparison_frontier_terminal line 154
  10. theorem OAI.EditApproximation.comparison_frontier_cost_slack line 166