OAI/Combinatorics/EditApproximation/Geometry/PrefixCosts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite prefix costs used by the predicted bands

A prefix is a restriction of an enumerated wide action. The last jump is evaluated at the proposed real shift. Taking the minimum over the actual finite list, with its first member duplicated as the fallback, gives the exact prefix minimum and its 1-Lipschitz property.

  1. def OAI.EditApproximation.realConnectionBudget line 19
  2. theorem OAI.EditApproximation.realConnectionBudget_finish_lipschitz line 24
  3. theorem OAI.EditApproximation.realConnectionBudget_cast line 42
  4. def OAI.EditApproximation.widePrefixCost line 50
  5. theorem OAI.EditApproximation.widePrefixCost_lipschitz line 57
  6. def OAI.EditApproximation.widePrefixMinimum line 69
  7. theorem OAI.EditApproximation.widePrefixMinimum_le_member line 75
  8. theorem OAI.EditApproximation.le_widePrefixMinimum line 82
  9. theorem OAI.EditApproximation.widePrefixMinimum_lipschitz line 93