OAI/Combinatorics/BinaryEdit/FiniteSourceFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TreeEdit.BinaryLower.exists_finite_source_family line 19

   Source documentation

   A finite-alphabet family with distortion constant 1/34, constructed from finite coordinate groups and their word images.

   theorem exists_finite_source_family :
       ∃ c₀ : ℝ, 0 < c₀ ∧ ∃ K : ℕ, ∀ k : ℕ, K ≤ k →
         ∃ Γ : Type, ∃ inst : Fintype Γ,
           1 ≤ @Fintype.card Γ inst ∧ @Fintype.card Γ inst ≤ finiteSourceLength k ∧
           ∃ W : Finset (Word Γ (finiteSourceLength k)), 2 ≤ W.card ∧
             c₀ * ((k : ℝ) / 4) ^ k ≤
               c1 {x : Word Γ (finiteSourceLength k) // x ∈ W}
                 (fun x y => (ed x.val.val y.val.val : ℝ)) := by
   …

   Mentions: OAI.TreeEdit.BinaryLower.finiteSourceLength, OAI.TreeEdit.Word, OAI.TreeEdit.ed