CodeEqualMatches.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Ordered equal-label bit matches can be colored by their ordinal modulo block width. This avoids the bipartite edge-coloring theorem in the source.

theorem OAI.TreeEdit.BinaryLower.Code.equal_match_count_le line 16
Source documentation
If every increasing block matching has at most L edges, then an increasing bit matching whose edges all join equal original labels has at most P * L edges. The hypothesis on each finite subset is precisely the longest-common- subsequence bound after the two block maps become strictly increasing.
```
theorem equal_match_count_le {N P L : ℕ} (hP : 0 < P)
    (f g : Fin N → ℕ) (hf : StrictMono f) (hg : StrictMono g)
    (hL : ∀ s : Finset (Fin N),
      StrictMonoOn (fun i => f i / P) (s : Set (Fin N)) →
      StrictMonoOn (fun i => g i / P) (s : Set (Fin N)) → s.card ≤ L) :
    N ≤ P * L := by
…
```

theorem OAI.TreeEdit.BinaryLower.Code.equal_label_match_count_le line 40

Source documentation

Concrete equal-label case of the modular coloring estimate. The strictly increasing lists f,g are the bit positions of the equal-label matches; their quotients index the original words.

theorem equal_label_match_count_le {α : Type*} {N P : ℕ} (hP : 0 < P)
    (x y : List α) (f g : Fin N → ℕ) (hf : StrictMono f) (hg : StrictMono g)
    (hfx : ∀ i, f i / P < x.length) (hgy : ∀ i, g i / P < y.length)
    (heq : ∀ i, x.get ⟨f i / P, hfx i⟩ = y.get ⟨g i / P, hgy i⟩) :
    N ≤ P * lcs x y := by
…

Mentions: OAI.TreeEdit.lcs

theorem OAI.TreeEdit.BinaryLower.Code.equal_label_subset_card_le line 62

Source documentation

The same estimate for a selected subset of a larger increasing bit matching. This is convenient when selecting exactly the equal-label edges.

theorem equal_label_subset_card_le {α : Type*} {N P : ℕ} (hP : 0 < P)
    (x y : List α) (f g : Fin N → ℕ) (hf : StrictMono f) (hg : StrictMono g)
    (hfx : ∀ i, f i / P < x.length) (hgy : ∀ i, g i / P < y.length)
    (s : Finset (Fin N))
    (heq : ∀ i ∈ s, x.get ⟨f i / P, hfx i⟩ = y.get ⟨g i / P, hgy i⟩) :
    s.card ≤ P * lcs x y := by
…

Mentions: OAI.TreeEdit.lcs