OAI/Combinatorics/BinaryEdit/TaggedArrayPrerequisites.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TreeEdit.BinaryLower.TaggedExtraction.local_slice_capacity line 14

   Source documentation

   A blockwise deficit bound gives the local slice capacity, with all slices taken from the actual nested concatenation.

   theorem local_slice_capacity {α : Type*} {T m B : ℕ}
       (X Y : Fin T → Fin m → Word α B) (tag : α → Fin m)
       (hX : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (X a i).val → tag s = i)
       (hY : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (Y a i).val → tag s = i)
       {d : ℝ} (hd : ∀ a b, d ≤ ∑ i, (deficit B (X a i).val (Y b i).val : ℝ))
       (a b : Fin T) :
       (lcs (((rows X).drop (a.val * (m * B))).take (m * B))
         (((rows Y).drop (b.val * (m * B))).take (m * B)) : ℝ) ≤
           (m : ℝ) * B - d := by
   …

   Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.lcs, OAI.TreeEdit.BinaryLower.TaggedExtraction.rows

2. theorem OAI.TreeEdit.BinaryLower.TaggedExtraction.exists_array_decoder line 31

   Source documentation

   Pairwise disjoint alphabets admit a common tag decoder.

   theorem exists_array_decoder {α : Type*} {T m B : ℕ}
       (X Y : Fin T → Fin m → Word α B) (hm : 0 < m)
       (Γ : Fin m → Set α) (hΓ : Pairwise fun i j => Disjoint (Γ i) (Γ j))
       (hX : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (X a i).val → s ∈ Γ i)
       (hY : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (Y a i).val → s ∈ Γ i) :
       ∃ tag : α → Fin m,
         (∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (X a i).val → tag s = i) ∧
         (∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (Y a i).val → tag s = i) := by
   …

   Mentions: OAI.TreeEdit.Word