OAI/Combinatorics/EditDistance/RowAlignment.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Charging arbitrary alignments across rows and markers

  1. def OAI.EditRows.payload line 12
  2. def OAI.EditRows.marker line 13
  3. lemma OAI.EditRows.mem_payload line 15
  4. lemma OAI.EditRows.mem_marker line 18
  5. lemma OAI.EditRows.card_payload line 22
  6. lemma OAI.EditRows.card_marker line 23
  7. lemma OAI.EditRows.payload_before line 25
  8. lemma OAI.EditRows.marker_disjoint line 32
  9. lemma OAI.EditRows.payload_disjoint line 43
  10. lemma OAI.EditRows.payload_subset_range line 50
  11. lemma OAI.EditRows.marker_subset_range line 58
  12. lemma OAI.EditRows.payload_index line 66
  13. lemma OAI.EditRows.payload_of_mod line 71
  14. lemma OAI.EditRows.marker_between line 77
  15. lemma OAI.EditRows.marker_not_payload line 85
  16. def OAI.EditRows.rowMatches line 101
  17. def OAI.EditRows.Cross line 104
  18. lemma OAI.EditRows.crossing_marker_unmatched line 108
  19. lemma OAI.EditRows.crossing_marker_distinct line 128
  20. lemma OAI.EditRows.sum_cards_le line 151
  21. lemma OAI.EditRows.noncross_loss line 164
  22. lemma OAI.EditRows.source_loss_card line 189
  23. lemma OAI.EditRows.unmatched_card line 203
  24. theorem OAI.EditRows.matching_loss line 213
  25. theorem OAI.EditRows.matching_loss_real line 285