OAI/Combinatorics/EditApproximation/Geometry/ComparisonTree.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The input-determined rounded comparison tree

The choices here are only for the proof. They use the exact input edit costs and a fixed classical choice of optimal alignment, and have no sampling argument. Stopped states are carried in child zero, with the remaining physical slots empty.

  1. abbrev OAI.EditApproximation.ComparisonState line 19
  2. def OAI.EditApproximation.comparisonStateCost line 21
  3. def OAI.EditApproximation.comparisonStopped line 26
  4. def OAI.EditApproximation.comparisonChildren line 30
  5. theorem OAI.EditApproximation.comparisonChildren_cost_bound line 39
  6. theorem OAI.EditApproximation.comparisonChildren_spec line 50
  7. theorem OAI.EditApproximation.comparisonChildren_lower line 69
  8. def OAI.EditApproximation.comparisonStep line 90
  9. theorem OAI.EditApproximation.comparisonStateCost_nonneg line 105
  10. theorem OAI.EditApproximation.comparisonStep_cost_bound line 112
  11. def OAI.EditApproximation.comparisonFrontier line 141
  12. theorem OAI.EditApproximation.comparison_frontier_cost_bound line 149
  13. theorem OAI.EditApproximation.comparison_frontier_cost_le_twice line 177