OAI/NumberTheory/EgyptianFractions/MarkedPrimeSupplyReduction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.quantitative_marked_length_of_prime_supply line 14

   Source documentation

   For the actual prime-factorial multiplier, the size estimate and positivity are theorems. The remaining prerequisites are precisely the rational-divisor supply and the quantitative marked prefix.

   theorem quantitative_marked_length_of_prime_supply
       (hsupply : ∀ᶠ m : ℕ in atTop,
         HasRationalDivisorSupply m (markedSupplyMultiplier m) 16)
       (hprefix : ∀ᶠ m : ℕ in atTop,
         HasQuantitativeMarkedPrefix m (markedSupplyMultiplier m)) :
       ∀ ε : ℝ, 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.HasQuantitativeMarkedPrefix, OAI.Problem337.IsOneExpansion