OAI/Combinatorics/EditDistance/WindowRecursion.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Dyadic-window recursion and insertion bounds

  1. def OAI.EditUpper.samples line 18
  2. def OAI.EditUpper.piece line 21
  3. lemma OAI.EditUpper.piece_nonneg line 25
  4. def OAI.EditUpper.lift line 29
  5. lemma OAI.EditUpper.lift_dist line 35
  6. lemma OAI.EditUpper.block_indel_bound line 47
  7. lemma OAI.EditUpper.block_lower line 54
  8. lemma OAI.EditUpper.lift_lower line 86
  9. lemma OAI.EditUpper.piece_insert_general line 104
  10. lemma OAI.EditUpper.piece_before line 130
  11. lemma OAI.EditUpper.piece_after line 139
  12. lemma OAI.EditUpper.sum_block_insert line 154
  13. lemma OAI.EditUpper.lift_insert_raw line 193
  14. lemma OAI.EditUpper.model_indel_lipschitz line 216