OAI/Combinatorics/EditDistance/RecursiveControl.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Averaged displacement control for recursive word families

  1. def OAI.EditFamily.weight line 18
  2. lemma OAI.EditFamily.weight_pos line 20
  3. lemma OAI.EditFamily.sum_weight line 29
  4. abbrev OAI.EditFamily.ProductState line 38
  5. def OAI.EditFamily.lift line 40
  6. def OAI.EditFamily.allPhase line 42
  7. lemma OAI.EditFamily.sum_lift_vectors line 44
  8. lemma OAI.EditFamily.lift_nsmul line 49
  9. lemma OAI.EditFamily.variation_zero line 56
  10. lemma OAI.EditFamily.component_control line 59
  11. theorem OAI.EditFamily.successor_control line 80