LCSEditUpper.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The deletion/insertion half of the source's edit--LCS comparison.

theorem OAI.TreeEdit.BinaryLower.editDistance_add_twice_lcs_le line 12
Source documentation
Ordinary edit distance is bounded by the insertion--deletion distance computed from a longest common subsequence.
```
theorem editDistance_add_twice_lcs_le {α : Type*} (x y : List α) :
    ed x y + 2 * lcs x y ≤ x.length + y.length := by
…
```
Mentions: OAI.TreeEdit.ed, OAI.TreeEdit.lcs
theorem OAI.TreeEdit.BinaryLower.editDistance_le_delta line 20
Source documentation
First inequality of source equation eq:metric-conversion.
```
theorem editDistance_le_delta {α : Type*} (x y : List α) :
    ed x y ≤ x.length + y.length - 2 * lcs x y := by
…
```
Mentions: OAI.TreeEdit.ed, OAI.TreeEdit.lcs
theorem OAI.TreeEdit.BinaryLower.editDistance_le_twice_deficit line 26
Source documentation
Upper inequality of source equation eq:deficit, on equal-length words.
```
theorem editDistance_le_twice_deficit {α : Type*} {n : ℕ} {x y : List α}
    (hx : x.length = n) (hy : y.length = n) :
    ed x y ≤ 2 * deficit n x y := by
…
```
Mentions: OAI.TreeEdit.ed, OAI.TreeEdit.BinaryLower.deficit