LCS.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Basic properties of the manuscript's exact longest-common-subsequence length. All maxima are attained by actual ordered sublists.

theorem OAI.TreeEdit.BinaryLower.lcs_nil_left line 16
theorem OAI.TreeEdit.BinaryLower.lcs_nil_right line 19
theorem OAI.TreeEdit.BinaryLower.lcs_mono_left line 22
theorem OAI.TreeEdit.BinaryLower.lcs_mono_right line 28
theorem OAI.TreeEdit.BinaryLower.lcs_eq_left_of_sublist line 34
theorem OAI.TreeEdit.BinaryLower.lcs_eq_length_iff line 38
theorem OAI.TreeEdit.BinaryLower.deficit_eq_zero_iff line 49
theorem OAI.TreeEdit.BinaryLower.one_le_deficit_of_ne line 61
theorem OAI.TreeEdit.BinaryLower.deficit_self line 67
theorem OAI.TreeEdit.BinaryLower.deficit_symm line 70
theorem OAI.TreeEdit.BinaryLower.lcs_overlap line 76
Source documentation
The overlap inequality underlying the triangle inequality for insertion-deletion distance.
```
theorem lcs_overlap (x y z : List α) :
    lcs x y + lcs y z ≤ y.length + lcs x z := by
…
```
Mentions: OAI.TreeEdit.lcs
theorem OAI.TreeEdit.BinaryLower.lcs_le_iff line 86
Source documentation
To bound the maximal matching size, it suffices to bound every common subsequence. This also avoids any appeal to an unattained supremum.
```
theorem lcs_le_iff {x y : List α} {n : ℕ} :
    lcs x y ≤ n ↔ ∀ z : List α, z.Sublist x → z.Sublist y → z.length ≤ n := by
…
```
Mentions: OAI.TreeEdit.lcs
theorem OAI.TreeEdit.BinaryLower.lcs_append_ge line 97
Source documentation
Concatenating two increasing matchings gives an increasing matching.
```
theorem lcs_append_ge (x₁ x₂ y₁ y₂ : List α) :
    lcs x₁ y₁ + lcs x₂ y₂ ≤ lcs (x₁ ++ x₂) (y₁ ++ y₂) := by
…
```
Mentions: OAI.TreeEdit.lcs
theorem OAI.TreeEdit.BinaryLower.lcs_append_left_le line 105
Source documentation
Splitting the source word partitions any common subsequence.
```
theorem lcs_append_left_le (x₁ x₂ y : List α) :
    lcs (x₁ ++ x₂) y ≤ lcs x₁ y + lcs x₂ y := by
…
```
Mentions: OAI.TreeEdit.lcs
theorem OAI.TreeEdit.BinaryLower.lcs_append_right_le line 114
theorem OAI.TreeEdit.BinaryLower.deficit_add_lcs line 118
theorem OAI.TreeEdit.BinaryLower.lcs_le_map line 125
Source documentation
Relabeling symbols cannot destroy a common subsequence.
```
theorem lcs_le_map {β : Type*} (f : α → β) (x y : List α) :
    lcs x y ≤ lcs (x.map f) (y.map f) := by
…
```
Mentions: OAI.TreeEdit.lcs
theorem OAI.TreeEdit.BinaryLower.lcs_map_injective line 133
Source documentation
Injective alphabet relabeling preserves the exact longest common subsequence length. No nonemptiness assumption on either alphabet is needed.
```
theorem lcs_map_injective {β : Type*} (f : α → β) (hf : Function.Injective f)
    (x y : List α) : lcs (x.map f) (y.map f) = lcs x y := by
…
```
Mentions: OAI.TreeEdit.lcs
theorem OAI.TreeEdit.BinaryLower.deficit_map_injective line 146