OAI/Combinatorics/EditDistance/Metric.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Unrestricted edit scripts, metric inequalities, and common subsequences

  1. def OAI.EditDistortion.indel line 14
  2. theorem OAI.EditDistortion.Step.symm line 21
  3. theorem OAI.EditDistortion.Step.map line 27
  4. theorem OAI.EditDistortion.Step.append_left line 35
  5. theorem OAI.EditDistortion.Step.append_right line 43
  6. theorem OAI.EditDistortion.Step.length_bounds line 55
  7. theorem OAI.EditDistortion.Step.allow_substitution line 59
  8. theorem OAI.EditDistortion.Script.trans line 69
  9. theorem OAI.EditDistortion.Script.single line 76
  10. theorem OAI.EditDistortion.Script.symm line 79
  11. theorem OAI.EditDistortion.Script.map line 84
  12. theorem OAI.EditDistortion.Script.append_left line 90
  13. theorem OAI.EditDistortion.Script.append_right line 96
  14. theorem OAI.EditDistortion.Script.to_nil line 102
  15. theorem OAI.EditDistortion.Script.exists_script line 107
  16. theorem OAI.EditDistortion.Script.eq_of_zero line 110
  17. theorem OAI.EditDistortion.Script.length_bounds line 114
  18. theorem OAI.EditDistortion.Script.allow_substitution line 120
  19. theorem OAI.EditDistortion.cost_le line 130
  20. theorem OAI.EditDistortion.cost_spec line 133
  21. theorem OAI.EditDistortion.cost_refl line 136
  22. theorem OAI.EditDistortion.cost_eq_zero_iff line 139
  23. theorem OAI.EditDistortion.cost_symm line 148
  24. theorem OAI.EditDistortion.cost_triangle line 153
  25. theorem OAI.EditDistortion.cost_map_le line 156
  26. theorem OAI.EditDistortion.cost_length_bounds line 160
  27. theorem OAI.EditDistortion.edit_le_indel line 164
  28. theorem OAI.EditDistortion.Step.indel_simulation line 174
  29. theorem OAI.EditDistortion.Script.indel_simulation line 183
  30. theorem OAI.EditDistortion.indel_le_two_edit line 192
  31. theorem OAI.EditDistortion.Script.max_length line 196
  32. theorem OAI.EditDistortion.edit_le_max_length line 208
  33. theorem OAI.EditDistortion.cost_map_eq_of_leftInverse line 211
  34. theorem OAI.EditDistortion.cost_append_le line 218
  35. theorem OAI.EditDistortion.Script.of_sublist line 222
  36. theorem OAI.EditDistortion.indel_le_matching_loss line 234
  37. theorem OAI.EditDistortion.sublist_erase_one line 251
  38. theorem OAI.EditDistortion.Script.common_sublist line 262
  39. theorem OAI.EditDistortion.indel_matching line 280
  40. theorem OAI.EditDistortion.le_indel_iff line 288