OAI/NumberTheory/EgyptianFractions/RoughDivisorAsymptotic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.eventually_rough_entropy_le_rpow line 13

   Source documentation

   At the logarithmic roughness threshold, the elementary entropy exponent for divisors of numbers of size exp (A log X log log X) is sublinear in log X. All estimates are uniform in the integer being factored.

   theorem eventually_rough_entropy_le_rpow (A ε : ℝ) (hA : 0 < A) (hε : 0 < ε) :
       ∀ᶠ X : ℝ in atTop,
         1 < X ∧ 1 < Real.log X ∧
         Real.log X ≤ A * Real.log X * Real.log (Real.log X) ∧
         Real.exp ((1 + Real.log
           ((A * Real.log X * Real.log (Real.log X)) / Real.log X)) *
             Real.log X / Real.log (Real.log X)) ≤ X ^ ε := by
   …

2. theorem OAI.Problem337.eventually_truncatedDivisorCount_rough_subpower line 60

   Source documentation

   Uniform subpower counting for logarithmically rough integers in the prime-product size window. Repeated prime factors are allowed.

   theorem eventually_truncatedDivisorCount_rough_subpower
       (A ε : ℝ) (hA : 0 < A) (hε : 0 < ε) :
       ∀ᶠ X : ℝ in atTop, ∀ n : ℕ, n ≠ 0 →
         Real.log (n : ℝ) ≤ A * Real.log X * Real.log (Real.log X) →
         (∀ p ∈ n.primeFactorsList, Real.log X ≤ (p : ℝ)) →
         (truncatedDivisorCount X n : ℝ) ≤ X ^ ε := by
   …

   Mentions: OAI.Problem337.truncatedDivisorCount