CoarsePadding.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Fresh-symbol right padding

Padding uses none, while original letters are tagged by some. Removing the fresh symbols contracts every unrestricted unit-cost edit script.

theorem OAI.EditApproximation.step_filterMap_script line 21

Source documentation

Removing or relabeling letters replaces each edit by at most one edit.

theorem step_filterMap_script {α : Type u} {β : Type v} {s : Bool}
    (f : α → Option β) {x y : List α} (step : Step s x y) :
    ∃ n ≤ 1, Script s n (x.filterMap f) (y.filterMap f) := by
…

theorem OAI.EditApproximation.script_filterMap line 44
theorem OAI.EditApproximation.edit_filterMap_le line 54
theorem OAI.EditApproximation.coarsePadTo_length line 63
Source documentation
Right padding to a prescribed common width with a fresh tagged letter.
```
theorem coarsePadTo_length {α : Type u} (n : ℕ) (word : List α) (h : word.length ≤ n) :
    (coarsePadTo n word).length = n := by
…
```
Mentions: OAI.EditApproximation.coarsePadTo
theorem OAI.EditApproximation.coarsePadTo_remove line 68

theorem OAI.EditApproximation.coarsePadding_distance_bounds line 74

Source documentation

The actual padded instance has distance between the original distance and twice that distance, including empty and unequal-length inputs.

theorem coarsePadding_distance_bounds {α : Type u} (x y : List α) :
    edit x y ≤ edit (coarsePadTo (max x.length y.length) x)
      (coarsePadTo (max x.length y.length) y) ∧
    edit (coarsePadTo (max x.length y.length) x)
      (coarsePadTo (max x.length y.length) y) ≤ 2 * edit x y := by
…

Mentions: OAI.EditApproximation.coarsePadTo