EditDeficit.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Both metric comparisons in the preliminary section, for the actual unrestricted unit-cost edit scripts and longest-common-subsequence definitions.

theorem OAI.TreeEdit.BinaryLower.delta_le_twice_editDistance line 13
Source documentation
Second inequality of source equation eq:metric-conversion.
```
theorem delta_le_twice_editDistance {α : Type*} (x y : List α) :
    x.length + y.length - 2 * lcs x y ≤ 2 * ed x y := by
…
```
Mentions: OAI.TreeEdit.lcs, OAI.TreeEdit.ed
theorem OAI.TreeEdit.BinaryLower.editDistance_delta_bounds line 21
Source documentation
Ordinary edit distance and insertion--deletion distance differ by at most factor two, without imposing a cap on intermediate script words.
```
theorem editDistance_delta_bounds {α : Type*} (x y : List α) :
    ed x y ≤ x.length + y.length - 2 * lcs x y ∧
      x.length + y.length - 2 * lcs x y ≤ 2 * ed x y :=
…
```
Mentions: OAI.TreeEdit.ed, OAI.TreeEdit.lcs
theorem OAI.TreeEdit.BinaryLower.deficit_le_editDistance line 27
Source documentation
Lower inequality of source equation eq:deficit, on equal-length words.
```
theorem deficit_le_editDistance {α : Type*} {n : ℕ} {x y : List α}
    (hx : x.length = n) (hy : y.length = n) :
    deficit n x y ≤ ed x y := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.ed
theorem OAI.TreeEdit.BinaryLower.editDistance_deficit_bounds line 36
Source documentation
The complete equal-length deficit comparison, including empty words.
```
theorem editDistance_deficit_bounds {α : Type*} {n : ℕ} {x y : List α}
    (hx : x.length = n) (hy : y.length = n) :
    deficit n x y ≤ ed x y ∧
      ed x y ≤ 2 * deficit n x y :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.ed

theorem OAI.TreeEdit.BinaryLower.editDistance_deficit_bounds_real line 43

Source documentation

Real-valued form used in the fixed-length binary conversion inequalities.

theorem editDistance_deficit_bounds_real {α : Type*} {n : ℕ} {x y : List α}
    (hx : x.length = n) (hy : y.length = n) :
    (deficit n x y : ℝ) ≤ (ed x y : ℝ) ∧
      (ed x y : ℝ) ≤ 2 * (deficit n x y : ℝ) := by
…

Mentions: OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.ed