CodeTrimming.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The local span-trimming step in fixed-length binary conversion

If a matched subsequence occupies two larger contiguous spans, taking prefixes of those spans deletes at most the total number of removed positions from the matching. This lemma does not assume that matched positions are consecutive.

theorem OAI.TreeEdit.BinaryLower.Code.common_sublist_take line 21

Source documentation

Trimming two words loses at most the sum of the numbers of removed symbols from any fixed common subsequence.

theorem common_sublist_take {α : Type u} {x y z : List α}
    (hzx : z.Sublist x) (hzy : z.Sublist y) (a b : ℕ) :
    ∃ w : List α, w.Sublist (x.take a) ∧ w.Sublist (y.take b) ∧
      z.length ≤ w.length + (x.length - a) + (y.length - b) := by
…

theorem OAI.TreeEdit.BinaryLower.Code.common_sublist_trim_to_matched_length line 34

Source documentation

The manuscript trims each span to the number of matched symbols.

theorem common_sublist_trim_to_matched_length {α : Type u} {x y z : List α}
    (hzx : z.Sublist x) (hzy : z.Sublist y) :
    ∃ w : List α, w.Sublist (x.take z.length) ∧ w.Sublist (y.take z.length) ∧
      z.length ≤ w.length + ((x.length - z.length) + (y.length - z.length)) := by
…

theorem OAI.TreeEdit.BinaryLower.Code.trim_separation_charge line 44

Source documentation

A 99-percent separation bound on the two trimmed segments charges at least one unmatched span position for each hundred matches. All arithmetic here is in natural numbers, avoiding rounding or division conventions.

theorem trim_separation_charge {α : Type u} {x y z : List α}
    (hzx : z.Sublist x) (hzy : z.Sublist y)
    (hsep : ∀ w : List α, w.Sublist (x.take z.length) →
      w.Sublist (y.take z.length) → 100 * w.length ≤ 99 * z.length) :
    z.length ≤ 100 * ((x.length - z.length) + (y.length - z.length)) := by
…

theorem OAI.TreeEdit.BinaryLower.Code.lcs_take_loss_le line 54
Source documentation
The trimming bound stated directly for the actual LCS maximum.
```
theorem lcs_take_loss_le {α : Type u} (x y : List α) (a b : ℕ) :
    lcs x y ≤ lcs (x.take a) (y.take b) + (x.length - a) + (y.length - b) := by
…
```
Mentions: OAI.TreeEdit.lcs

theorem OAI.TreeEdit.BinaryLower.Code.trim_separation_charge_lcs line 63

Source documentation

A version of the local charge which accepts the segment code's LCS separation hypothesis directly.

theorem trim_separation_charge_lcs {α : Type u} {x y z : List α}
    (hzx : z.Sublist x) (hzy : z.Sublist y)
    (hsep : 100 * lcs (x.take z.length) (y.take z.length) ≤ 99 * z.length) :
    z.length ≤ 100 * ((x.length - z.length) + (y.length - z.length)) := by
…

Mentions: OAI.TreeEdit.lcs

theorem OAI.TreeEdit.BinaryLower.Code.trim_separation_charge_real line 72

Source documentation

Real-valued form of the source's g ≥ 0.01 a charge.

theorem trim_separation_charge_real {α : Type u} {x y z : List α}
    (hzx : z.Sublist x) (hzy : z.Sublist y)
    (hsep : 100 * lcs (x.take z.length) (y.take z.length) ≤ 99 * z.length) :
    (z.length : ℝ) / 100 ≤
      ((x.length - z.length : ℕ) : ℝ) + ((y.length - z.length : ℕ) : ℝ) := by
…

Mentions: OAI.TreeEdit.lcs