OAI/Combinatorics/BinaryEdit/FiniteParameters.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TreeEdit.BinaryLower.Parameters.finiteLength line 8

   Source documentation

   Binary word length for the quadratic-width code, with source length (20 * k * k^(20*k))^k.

   def finiteLength (k : ℕ) : ℕ := (20 * k * k ^ (20 * k)) ^ (3 * k)

2. lemma OAI.TreeEdit.BinaryLower.Parameters.finiteLength_pos line 10
3. lemma OAI.TreeEdit.BinaryLower.Parameters.log_finiteLength line 14
4. lemma OAI.TreeEdit.BinaryLower.Parameters.finiteLength_log_succ_le line 25
5. lemma OAI.TreeEdit.BinaryLower.Parameters.le_finiteLength line 70
6. lemma OAI.TreeEdit.BinaryLower.Parameters.finiteLength_log_succ_pos line 77
7. lemma OAI.TreeEdit.BinaryLower.Parameters.finiteLength_loglog_succ_le line 83
8. lemma OAI.TreeEdit.BinaryLower.Parameters.finite_lower_log_bound line 104
9. lemma OAI.TreeEdit.BinaryLower.Parameters.eventually_finite_lower_log_bound line 123
10. lemma OAI.TreeEdit.BinaryLower.Parameters.finite_cap_sqrt_bound line 134

    Source documentation

    The logarithmic scale at any cap below the next construction length.

    lemma finite_cap_sqrt_bound {k d : ℕ} (hk : 20 ≤ k) (hd : 2 ≤ d)
        (hcap : d ≤ finiteLength (k + 1)) :
        Real.sqrt (Real.log (d : ℝ) * Real.log (Real.log (d : ℝ))) ≤
          40 * k * Real.log k := by
    …

    Mentions: OAI.TreeEdit.BinaryLower.Parameters.finiteLength

11. lemma OAI.TreeEdit.BinaryLower.Parameters.finite_cap_exponential_bound line 159

    Source documentation

    Numerical transfer from a finite-family distortion to an intervening cap.

    lemma finite_cap_exponential_bound {c₀ : ℝ} (hc₀ : 0 < c₀) {k d : ℕ}
        (hk : 20 ≤ k) (hkc : -4 * Real.log c₀ ≤ (k : ℝ))
        (hd : 2 ≤ d) (hcap : d ≤ finiteLength (k + 1)) :
        Real.exp ((1 / 160 : ℝ) *
          Real.sqrt (Real.log (d : ℝ) * Real.log (Real.log (d : ℝ)))) ≤
            c₀ * ((k : ℝ) / 4) ^ k := by
    …

    Mentions: OAI.TreeEdit.BinaryLower.Parameters.finiteLength

12. lemma OAI.TreeEdit.BinaryLower.Parameters.exists_finiteLength_bracket line 178

    Source documentation

    Choose adjacent construction lengths bracketing a cap. No strict monotonicity of the length sequence is needed for this selection argument.

    lemma exists_finiteLength_bracket {k₀ d : ℕ} (hk₀ : 0 < k₀)
        (hd : finiteLength k₀ ≤ d) :
        ∃ k : ℕ, k₀ ≤ k ∧ finiteLength k ≤ d ∧ d < finiteLength (k + 1) := by
    …

    Mentions: OAI.TreeEdit.BinaryLower.Parameters.finiteLength

13. lemma OAI.TreeEdit.BinaryLower.Parameters.exists_finite_cap_parameters line 197

    Source documentation

    The complete numerical all-large-cap selection used after constructing the finite-tree witness family. The requested lower threshold K is arbitrary.

    lemma exists_finite_cap_parameters {c₀ : ℝ} (hc₀ : 0 < c₀) (K : ℕ) :
        ∃ d₀ : ℕ, ∀ d ≥ d₀, ∃ k : ℕ,
          K ≤ k ∧ 20 ≤ k ∧ finiteLength k ≤ d ∧
            Real.exp ((1 / 160 : ℝ) *
              Real.sqrt (Real.log (d : ℝ) * Real.log (Real.log (d : ℝ)))) ≤
                c₀ * ((k : ℝ) / 4) ^ k := by
    …

    Mentions: OAI.TreeEdit.BinaryLower.Parameters.finiteLength