CodeConversion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The exact arithmetic and metric estimates for fixed-length binary conversion.

theorem OAI.TreeEdit.BinaryLower.Code.encode_bounds_of_deficit line 16

Source documentation

The precise 402 deficit estimate implies the required 804 ordinary-edit estimate for a fixed pair of original words. Both metrics are the actual unrestricted unit-cost edit distance.

theorem encode_bounds_of_deficit {α : Type u} {β : Type v} {M P : ℕ}
    (c : α → Word β P) {x y : List α}
    (hx : x.length = M) (hy : y.length = M)
    (hdef : (P : ℝ) / 402 * (deficit M x y : ℝ) ≤
      (deficit (M * P) (encode c x) (encode c y) : ℝ)) :
    (P : ℝ) / 804 * (ed x y : ℝ) ≤
        (ed (encode c x) (encode c y) : ℝ) ∧
      (ed (encode c x) (encode c y) : ℝ) ≤
        (P : ℝ) * (ed x y : ℝ) := by
…

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

theorem OAI.TreeEdit.BinaryLower.Code.encode_bounds_of_additive line 35

Source documentation

A code satisfying the additive block-pair estimate, with short-pair error at most half a block, has both advertised inequalities and the stronger one-sided-deficit inequality. The zero-deficit case is included.

theorem encode_bounds_of_additive {α : Type u} {β : Type v}
    {M P error : ℕ} (c : α → Word β P) {x y : List α}
    (hx : x.length = M) (hy : y.length = M)
    (hadd : P * deficit M x y ≤
      201 * deficit (M * P) (encode c x) (encode c y) + error)
    (herr : 2 * error ≤ P) :
    ((P : ℝ) / 804 * (ed x y : ℝ) ≤
        (ed (encode c x) (encode c y) : ℝ) ∧
      (ed (encode c x) (encode c y) : ℝ) ≤
        (P : ℝ) * (ed x y : ℝ)) ∧
    (P : ℝ) / 402 * (deficit M x y : ℝ) ≤
      (deficit (M * P) (encode c x) (encode c y) : ℝ) := by
…

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

theorem OAI.TreeEdit.BinaryLower.Code.natural_short_pair_error line 52
Source documentation
The source's real-valued short-pair threshold gives its integer loss budget without rounding changes.
```
theorem natural_short_pair_error {M : ℕ}
    (h : 2 * (M : ℝ) * segmentThreshold M ≤ (M : ℝ) ^ 2 / 2) :
    2 * (2 * M * segmentThreshold M) ≤ M ^ 2 := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.Code.segmentThreshold