OAI/Combinatorics/BinaryEdit/FiniteCapTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TreeEdit.BinaryLower.binary_lower_bound_of_finite_family line 11

   Source documentation

   Apply the numerical cap interpolation to actual finite sets of binary words. The hypothesis is exactly the output needed from the finite-tree obstruction followed by the fixed-length binary code.

   theorem binary_lower_bound_of_finite_family
       (hfamily : ∃ c₀ : ℝ, 0 < c₀ ∧ ∃ K : ℕ, ∀ k : ℕ, K ≤ k →
         ∃ W : Finset (Word Bool (Parameters.finiteLength k)),
           2 ≤ W.card ∧ c₀ * ((k : ℝ) / 4) ^ k ≤ binarySetDistortion W) :
       ∃ c : ℝ, 0 < c ∧ ∃ d₀ : ℕ, ∀ d : ℕ, d₀ ≤ d →
         ∃ n : ℕ, 1 ≤ n ∧ n ≤ d ∧
           ∃ W : Finset (Word Bool n), 2 ≤ W.card ∧
             growth c d ≤ binarySetDistortion W := by
   …

   Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.Parameters.finiteLength