Geometry.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Interval-state edit geometry

The edit distance here is the repository's unrestricted unit-cost insertion/deletion/substitution distance, not an abstract metric supplied as a hypothesis. These are the length and endpoint bounds in Section 2.

theorem OAI.EditApproximation.substring_length line 24
Source documentation
The target substring with boundary indices lo and hi.
```
theorem substring_length {α : Type u} (word : List α) (lo hi : ℕ)
    (hhi : hi ≤ word.length) : (substring word lo hi).length = hi - lo := by
…
```
Mentions: OAI.EditApproximation.substring
theorem OAI.EditApproximation.edit_sublist_le line 28
theorem OAI.EditApproximation.edit_drop_indices_le line 32
theorem OAI.EditApproximation.edit_substring_right_le line 46
theorem OAI.EditApproximation.edit_substring_endpoints_le line 62
Source documentation
Changing both substring endpoints costs at most their total movement, including when the two intervals are disjoint.
```
theorem edit_substring_endpoints_le {α : Type u} (word : List α)
    (lo hi lo' hi' : ℕ) :
    edit (substring word lo hi) (substring word lo' hi') ≤
      Nat.dist lo lo' + Nat.dist hi hi' := by
…
```
Mentions: OAI.EditApproximation.substring
theorem OAI.EditApproximation.abs_length_gap_le_edit line 71

theorem OAI.EditApproximation.interval_cost_lipschitz line 79

Source documentation

The actual interval-state cost is 1-Lipschitz in the endpoint metric.

theorem interval_cost_lipschitz {α : Type u} (x y : List α)
    (lo hi lo' hi' : ℕ) :
    |(edit x (substring y lo hi) : ℝ) - edit x (substring y lo' hi')| ≤
      (Nat.dist lo lo' + Nat.dist hi hi' : ℕ) := by
…

Mentions: OAI.EditApproximation.substring

theorem OAI.EditApproximation.edit_le_total_length line 101