FiniteFamilyTransfer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TreeEdit.BinaryLower.finiteSourceLength line 12
Source documentation
Original word length before the quadratic-width binary conversion.
```
def finiteSourceLength (k : ℕ) : ℕ := (20 * k * k ^ (20 * k)) ^ k
```
lemma OAI.TreeEdit.BinaryLower.le_finiteSourceLength line 14
lemma OAI.TreeEdit.BinaryLower.finiteSourceLength_mul_sq line 21

theorem OAI.TreeEdit.BinaryLower.binary_lower_bound_of_finite_source_family line 31

Source documentation

A finite-alphabet lower bound transfers to the all-cap binary lower bound through a fixed-width binary code.

theorem binary_lower_bound_of_finite_source_family
    (hcode : ∃ M₀ : ℕ, ∀ M : ℕ, M₀ ≤ M →
      ∀ (Γ : Type u) [Fintype Γ],
        1 ≤ Fintype.card Γ → Fintype.card Γ ≤ M →
        ∃ c : Γ → Word Bool (M ^ 2), ∀ x y : Word Γ M,
          (((M ^ 2 : ℕ) : ℝ) / 804) * (ed x.val y.val : ℝ) ≤
            (ed (encode c x.val) (encode c y.val) : ℝ))
    (hfamily : ∃ c₀ : ℝ, 0 < c₀ ∧ ∃ K : ℕ, ∀ k : ℕ, K ≤ k →
      ∃ Γ : Type u, ∃ inst : Fintype Γ,
        1 ≤ @Fintype.card Γ inst ∧ @Fintype.card Γ inst ≤ finiteSourceLength k ∧
        ∃ W : Finset (Word Γ (finiteSourceLength k)), 2 ≤ W.card ∧
          c₀ * ((k : ℝ) / 4) ^ k ≤
…

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