OAI/Combinatorics/BinaryEdit/SegmentCodeLCS.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TreeEdit.BinaryLower.SegmentCode.ofFn_window line 10

   Source documentation

   Array windows coincide with actual contiguous list segments.

   theorem ofFn_window {α : Type*} {P : ℕ} (b : Fin P → α)
       (a i : ℕ) (hi : i+a ≤ P) :
       List.ofFn (fun t : Fin a => b (window a i hi t)) =
         ((List.ofFn b).drop i).take a := by
   …

   Mentions: OAI.TreeEdit.BinaryLower.SegmentCode.window

2. theorem OAI.TreeEdit.BinaryLower.SegmentCode.SegmentSeparated.lcs_le line 23

   Source documentation

   The simultaneous increasing-matching property bounds the actual LCS of contiguous codeword segments.

   theorem SegmentSeparated.lcs_le {K P a₀ : ℕ} {c : Fin K → Fin P → Bool}
       (hc : SegmentSeparated c a₀) (k l : Fin K) (hkl : k ≠ l)
       (a i j : ℕ) (ha : a₀ ≤ a) (hi : i+a ≤ P) (hj : j+a ≤ P) :
       100 * lcs (((List.ofFn (c k)).drop i).take a)
         (((List.ofFn (c l)).drop j).take a) ≤ 99*a := by
   …

   Mentions: OAI.TreeEdit.BinaryLower.SegmentCode.SegmentSeparated, OAI.TreeEdit.lcs

3. theorem OAI.TreeEdit.BinaryLower.SegmentCode.exists_lcs_separated_code line 44

   Source documentation

   The codebook construction for an arbitrary finite alphabet, using the canonical concrete word type and the actual longest common subsequence.

   theorem exists_lcs_separated_code (Γ : Type*) [Fintype Γ] (P a₀ : ℕ)
       (hprob : (Fintype.card Γ : ℝ)^2 * ((P+1 : ℕ) : ℝ)^3 *
         (9/10 : ℝ)^a₀ < 1) :
       ∃ c : Γ → Word Bool P,
         ∀ (k l : Γ), k ≠ l → ∀ (a i j : ℕ), a₀ ≤ a →
           i+a ≤ P → j+a ≤ P →
             100 * lcs (((c k).val.drop i).take a) (((c l).val.drop j).take a) ≤ 99*a := by
   …

   Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.lcs

4. theorem OAI.TreeEdit.BinaryLower.SegmentCode.exists_lcs_separated_code_real line 60

   Source documentation

   Real-valued separation convention LCS ≤ 0.99 a used in the manuscript.

   theorem exists_lcs_separated_code_real (Γ : Type*) [Fintype Γ] (P a₀ : ℕ)
       (hprob : (Fintype.card Γ : ℝ)^2 * ((P+1 : ℕ) : ℝ)^3 *
         (9/10 : ℝ)^a₀ < 1) :
       ∃ c : Γ → Word Bool P,
         ∀ (k l : Γ), k ≠ l → ∀ (a i j : ℕ), a₀ ≤ a →
           i+a ≤ P → j+a ≤ P →
             (lcs (((c k).val.drop i).take a) (((c l).val.drop j).take a) : ℝ) ≤
               (99/100 : ℝ) * a := by
   …

   Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.lcs