BlockRestriction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Restricting increasing common matchings to arbitrary contiguous intervals.

theorem OAI.TreeEdit.BinaryLower.BlockRestriction.card_le_lcs_slices line 19

Source documentation

Restriction to any selected set of matched pairs lying in two specified intervals has size at most the LCS of the corresponding list slices. The intervals may touch or exceed the list boundary; no artificial positivity or nonempty-matching assumption is needed.

theorem card_le_lcs_slices (x y : List α) {n : ℕ}
    (u v : Fin n → ℕ) (hu : StrictMono u) (hv : StrictMono v)
    (hxu : ∀ t, u t < x.length) (hyv : ∀ t, v t < y.length)
    (heq : ∀ t, x[u t]'(hxu t) = y[v t]'(hyv t))
    (s : Finset (Fin n)) (a b A B : ℕ)
    (hsu : ∀ t ∈ s, a ≤ u t ∧ u t < a + A)
    (hsv : ∀ t ∈ s, b ≤ v t ∧ v t < b + B) :
    s.card ≤ lcs ((x.drop a).take A) ((y.drop b).take B) := by
…

Mentions: OAI.TreeEdit.lcs

lemma OAI.TreeEdit.BinaryLower.BlockRestriction.row_bounds line 63
Source documentation
The quotient convention in the tagged-row proof identifies a contiguous interval of width m * B; the order p / B / m is retained literally.
```
lemma row_bounds {p m B r : ℕ} (hm : 0 < m) (hB : 0 < B)
    (hrow : p / B / m = r) :
    r * (m * B) ≤ p ∧ p < r * (m * B) + m * B := by
…
```

theorem OAI.TreeEdit.BinaryLower.BlockRestriction.card_filter_rows_le_lcs line 74

Source documentation

The exact row-pair restriction used in ordered-tag matching arguments. No row-boundary alignment of the original matching is assumed.

theorem card_filter_rows_le_lcs (x y : List α) {n : ℕ}
    (u v : Fin n → ℕ) (hu : StrictMono u) (hv : StrictMono v)
    (hxu : ∀ t, u t < x.length) (hyv : ∀ t, v t < y.length)
    (heq : ∀ t, x[u t]'(hxu t) = y[v t]'(hyv t))
    (m B a b : ℕ) (hm : 0 < m) (hB : 0 < B) :
    (Finset.univ.filter (fun t => u t / B / m = a ∧ v t / B / m = b)).card ≤
      lcs ((x.drop (a * (m * B))).take (m * B))
        ((y.drop (b * (m * B))).take (m * B)) := by
…

Mentions: OAI.TreeEdit.lcs