TaggedRowLCS.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Longest common subsequence bounds for rows over disjoint tagged alphabets.

def OAI.TreeEdit.BinaryLower.TaggedRow.row line 12
Source documentation
Concatenation in increasing block-index order.
```
def row {α : Type*} {m : ℕ} (blocks : Fin m → List α) : List α :=
…
```
theorem OAI.TreeEdit.BinaryLower.TaggedRow.row_eq_flatten_ofFn line 15
theorem OAI.TreeEdit.BinaryLower.TaggedRow.flatMap_single_index line 19
theorem OAI.TreeEdit.BinaryLower.TaggedRow.filter_row line 34

theorem OAI.TreeEdit.BinaryLower.TaggedRow.sum_length_filter_tag line 57

Source documentation

Tag fibers partition every finite word's positions.

theorem sum_length_filter_tag {α I : Type*} [Fintype I] [DecidableEq I]
    (tag : α → I) (z : List α) :
    (∑ i, (z.filter (fun a => decide (tag a = i))).length) = z.length := by
…

theorem OAI.TreeEdit.BinaryLower.TaggedRow.common_sublist_length_le_sum_lcs line 73

Source documentation

Common subsequences of rows are bounded by the sum of block LCS lengths.

theorem common_sublist_length_le_sum_lcs {α : Type*} {m : ℕ}
    (tag : α → Fin m) (X Y : Fin m → List α)
    (hX : ∀ i, ∀ a ∈ X i, tag a = i)
    (hY : ∀ i, ∀ a ∈ Y i, tag a = i)
    {z : List α} (hzX : z.Sublist (row X)) (hzY : z.Sublist (row Y)) :
    z.length ≤ ∑ i, lcs (X i) (Y i) := by
…

Mentions: OAI.TreeEdit.BinaryLower.TaggedRow.row, OAI.TreeEdit.lcs

theorem OAI.TreeEdit.BinaryLower.TaggedRow.lcs_row_le_sum line 89

Source documentation

Local row bound used in the nonsplit-row argument.

theorem lcs_row_le_sum {α : Type*} {m : ℕ}
    (tag : α → Fin m) (X Y : Fin m → List α)
    (hX : ∀ i, ∀ a ∈ X i, tag a = i)
    (hY : ∀ i, ∀ a ∈ Y i, tag a = i) :
    lcs (row X) (row Y) ≤ ∑ i, lcs (X i) (Y i) := by
…

Mentions: OAI.TreeEdit.lcs, OAI.TreeEdit.BinaryLower.TaggedRow.row

theorem OAI.TreeEdit.BinaryLower.TaggedRow.length_row line 101
Source documentation
Exact length of an equal-block row.
```
theorem length_row {α : Type*} {m B : ℕ} (X : Fin m → List α)
    (hX : ∀ i, (X i).length = B) : (row X).length = m * B := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.TaggedRow.row

theorem OAI.TreeEdit.BinaryLower.TaggedRow.sum_deficit_le_row_deficit line 107

Source documentation

Tagwise deficits accumulate in a single pair of rows. This is the local deficit estimate consumed by the nonsplit-row counting argument.

theorem sum_deficit_le_row_deficit {α : Type*} {m B : ℕ}
    (tag : α → Fin m) (X Y : Fin m → List α)
    (hX : ∀ i, ∀ a ∈ X i, tag a = i)
    (hY : ∀ i, ∀ a ∈ Y i, tag a = i)
    (hXL : ∀ i, (X i).length = B) :
    (∑ i, deficit B (X i) (Y i)) ≤ deficit (m * B) (row X) (row Y) := by
…

Mentions: OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.BinaryLower.TaggedRow.row

theorem OAI.TreeEdit.BinaryLower.TaggedRow.lcs_row_le_capacity_sub line 128

Source documentation

Real-valued LCS row capacity, convenient when a separate matching restriction lemma has already bounded a row-pair count by its LCS.

theorem lcs_row_le_capacity_sub {α : Type*} {m B : ℕ}
    (tag : α → Fin m) (X Y : Fin m → List α)
    (hX : ∀ i, ∀ a ∈ X i, tag a = i)
    (hY : ∀ i, ∀ a ∈ Y i, tag a = i)
    (hXL : ∀ i, (X i).length = B)
    {d : ℝ} (hd : d ≤ ∑ i, (deficit B (X i) (Y i) : ℝ)) :
    (lcs (row X) (row Y) : ℝ) ≤ (m : ℝ) * B - d := by
…

Mentions: OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.lcs, OAI.TreeEdit.BinaryLower.TaggedRow.row

theorem OAI.TreeEdit.BinaryLower.TaggedRow.common_sublist_length_le_capacity_sub line 147

Source documentation

Real-valued version matching the manuscript's local row-loss hypothesis.

theorem common_sublist_length_le_capacity_sub {α : Type*} {m B : ℕ}
    (tag : α → Fin m) (X Y : Fin m → List α)
    (hX : ∀ i, ∀ a ∈ X i, tag a = i)
    (hY : ∀ i, ∀ a ∈ Y i, tag a = i)
    (hXL : ∀ i, (X i).length = B)
    {d : ℝ} (hd : d ≤ ∑ i, (deficit B (X i) (Y i) : ℝ))
    {z : List α} (hzX : z.Sublist (row X)) (hzY : z.Sublist (row Y)) :
    (z.length : ℝ) ≤ (m : ℝ) * B - d := by
…

Mentions: OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.BinaryLower.TaggedRow.row

theorem OAI.TreeEdit.BinaryLower.TaggedRow.exists_tag_of_pairwise_disjoint line 174
Source documentation
Pairwise disjoint alphabets admit a tag on the ambient alphabet. Values outside their union are irrelevant and receive an arbitrary default tag.
```
theorem exists_tag_of_pairwise_disjoint {α I : Type*} [Nonempty I]
    (Γ : I → Set α) (hΓ : Pairwise fun i j => Disjoint (Γ i) (Γ j)) :
    ∃ tag : α → I, ∀ i, ∀ a ∈ Γ i, tag a = i := by
…
```

theorem OAI.TreeEdit.BinaryLower.TaggedRow.lcs_row_le_sum_of_disjoint line 190

Source documentation

The row LCS bound stated directly for the manuscript's pairwise disjoint alphabets, without asking the caller to provide a tag function.

theorem lcs_row_le_sum_of_disjoint {α : Type*} {m : ℕ} (hm : 0 < m)
    (Γ : Fin m → Set α)
    (hΓ : Pairwise fun i j => Disjoint (Γ i) (Γ j))
    (X Y : Fin m → List α)
    (hX : ∀ i, ∀ a ∈ X i, a ∈ Γ i)
    (hY : ∀ i, ∀ a ∈ Y i, a ∈ Γ i) :
    lcs (row X) (row Y) ≤ ∑ i, lcs (X i) (Y i) := by
…

Mentions: OAI.TreeEdit.lcs, OAI.TreeEdit.BinaryLower.TaggedRow.row