EncodingUpper.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TreeEdit.BinaryLower.encode_editDistance_le_real line 11

Source documentation

The real-valued form of the upper estimate used in thm:804.

theorem encode_editDistance_le_real {α : Type u} {β : Type v} {P : ℕ}
    (c : α → Word β P) (x y : List α) :
    (ed (encode c x) (encode c y) : ℝ) ≤
      (P : ℝ) * (ed x y : ℝ) := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.ed, OAI.TreeEdit.encode

theorem OAI.TreeEdit.BinaryLower.length_encode_cube line 18
Source documentation
Width M² and input length M give output length exactly M³.
```
theorem length_encode_cube {α : Type u} {β : Type v} {M : ℕ}
    (c : α → Word β (M ^ 2)) (x : Word α M) :
    (encode c x.val).length = M ^ 3 := by
…
```
Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.encode