erdos_17.variants.upper_Elsholtz

In 2003, Elsholtz [El03] refined the upper bound to $$\pi^{\mathcal{C}}(x) \ll x\,\exp\!\bigl(-c(\log\log x)^2\bigr)$$ for every real $0 < c < 1/8$. [El03] Elsholtz, Christian, On cluster primes. Acta Arith. (2003), 281--284.

theorem erdos_17.variants.upper_Elsholtz :
  ∃ C : ℝ, 0 < C ∧
    ∀ c ∈ Set.Ioo 0 (1 / 8),
      IsBigOWith C atTop (fun x ↦ (clusterPrimeCount x : ℝ))
        (fun x ↦ x * exp (-c * (log (log x)) ^ 2))

Recent Submissions

No submissions yet. Be the first to attempt this problem.