Leaves.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

An occurrence query gives the exact unit-cost edit distance at a source leaf of width one (Section 2 of the manuscript).

theorem OAI.EditApproximation.occurrenceDeficit_le_length line 23
Source documentation
The part of the singleton cost determined by length and occurrence.
```
theorem occurrenceDeficit_le_length {α : Type u} [DecidableEq α]
    (a : α) (word : List α) : occurrenceDeficit a word ≤ word.length := Nat.sub_le _ _
```
Mentions: OAI.EditApproximation.occurrenceDeficit
theorem OAI.EditApproximation.length_le_occurrenceDeficit_add_one line 26
theorem OAI.EditApproximation.occurrenceDeficit_step line 32
Source documentation
One edit can increase the occurrence deficit by at most one.
```
theorem occurrenceDeficit_step {α : Type u} [DecidableEq α]
    (a : α) {x y : List α} (h : Step true x y) :
    occurrenceDeficit a y ≤ occurrenceDeficit a x + 1 := by
…
```
Mentions: OAI.EditApproximation.occurrenceDeficit
theorem OAI.EditApproximation.occurrenceDeficit_script line 59
theorem OAI.EditApproximation.occurrenceDeficit_le_singleton_edit line 68
theorem OAI.EditApproximation.singletonCost_eq_edit line 76
Source documentation
Executable exact answer for a source interval containing one symbol.
```
theorem singletonCost_eq_edit {α : Type u} [DecidableEq α]
    (a : α) (word : List α) : singletonCost a word = edit [a] word := by
…
```
Mentions: OAI.EditApproximation.singletonCost