OAI/NumberTheory/EgyptianFractions/MarkedFinalReduction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.quantitative_marked_length_of_eventual_prime_supply line 14

   Source documentation

   All arithmetic prefix, grouping, distinctness, and analytic length work is proved. The remaining input is the eventual rational-divisor supply for the specific prime-factorial multiplier.

   theorem quantitative_marked_length_of_eventual_prime_supply
       (hsupply : ∀ᶠ m : ℕ in atTop,
         HasRationalDivisorSupply m (markedSupplyMultiplier m) 16) :
       ∀ ε : ℝ, 0 < ε → ∃ M : ℕ, 2 ≤ M ∧
         ∀ m : ℕ, M ≤ m → ∃ k : ℕ, ∃ n : Fin k → ℕ,
           IsOneExpansion n ∧ (∃ i, n i = m) ∧
           (k : ℝ) ≤ (257 / Real.log 2 + ε) * Real.log (Real.log (m : ℝ)) := by
   …

   Mentions: OAI.Problem337.HasRationalDivisorSupply, OAI.Problem337.markedSupplyMultiplier, OAI.Problem337.IsOneExpansion