OAI/NumberTheory/EgyptianFractions/MarkedQuantitative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.quantitative_marked_length_of_explicit_budget line 13

   Source documentation

   A final reduction of the quantitative marked target to the explicit construction bounds, before asymptotic error absorption.

   theorem quantitative_marked_length_of_explicit_budget (K : ℕ → ℝ)
       (hKpositive : ∀ᶠ m : ℕ in atTop, 1 ≤ K m)
       (hK : ∀ δ : ℝ, 0 < δ → ∀ᶠ m : ℕ in atTop,
         Real.log (K m) ≤ (32 / Real.log 2 + δ) * Real.log (m : ℝ) *
           Real.log (Real.log (m : ℝ)))
       (hconstruct : ∀ᶠ m : ℕ in atTop,
         ∃ j t k : ℕ, ∃ n : Fin k → ℕ,
           IsOneExpansion n ∧ (∃ i, n i = m) ∧ k ≤ 1 + j + t ∧
           (j : ℝ) ≤ 3 + (Real.log (Real.log (2 * (m : ℝ) * K m)) -
             Real.log (Real.log 2)) / Real.log 2 ∧
           (t : ℝ) ≤ 16 * ((Real.log (K m) + Real.log (2 * (m : ℝ))) /
             (2 * Real.log (m : ℝ)) + 2)) :
   …

   Mentions: OAI.Problem337.IsOneExpansion