OAI/Combinatorics/EditDistance/Windows.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Padded windows and insertion-deletion matching inequalities

  1. def OAI.EditWindow.window line 14
  2. lemma OAI.EditWindow.window_length line 17
  3. lemma OAI.EditWindow.lookup_insert_before line 20
  4. lemma OAI.EditWindow.lookup_insert_after line 24
  5. lemma OAI.EditWindow.window_before line 30
  6. lemma OAI.EditWindow.window_after line 37
  7. theorem OAI.EditWindow.window_insert_cost line 45
  8. lemma OAI.EditDistortion.indel_cost line 82
  9. lemma OAI.EditDistortion.step_indel_filterMap line 84
  10. lemma OAI.EditDistortion.indel_filterMap_le line 101
  11. def OAI.EditWindow.segment line 119
  12. lemma OAI.EditWindow.segment_length line 122
  13. lemma OAI.EditWindow.segment_sublist line 125
  14. lemma OAI.EditWindow.segment_loss line 133
  15. lemma OAI.EditWindow.segment_cross line 137
  16. lemma OAI.EditWindow.segment_append line 151
  17. lemma OAI.EditWindow.indel_segment_blocks line 160
  18. lemma OAI.EditWindow.window_eq_segment line 170
  19. lemma OAI.EditWindow.window_padding line 173
  20. lemma OAI.EditWindow.filterMap_window line 187
  21. lemma OAI.EditWindow.indel_le_window line 192