Erdős Problem 726

References:

• erdosproblems.com/726
• [EGRS75] Erdős, P., and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of $(\sp{2n}\sb{n})$. Math. Comp. (1975), 83-92.

theorem Erdos726.erdos_726 : sorry ↔ Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ∑ p ∈ Finset.range (n + 1) with Nat.Prime p ∧ ↑p / 2 < ↑n % ↑p, 1 / ↑p) fun (n : ℕ) => Real.log (Real.log ↑n) / 2

As $n\to \infty$ ranges over integers $\sum_{p\leq n}1_{n\in (p/2,p)\pmod{p}}\frac{1}{p}\sim \frac{\log\log n}{2}$?

A conjecture of Erdős, Graham, Ruzsa, and Straus [EGRS75].

By $n\in (p/2,p)\pmod{p}$ we mean $n\equiv r\pmod{p}$ for some integer $r$ with $p/2<r<p$.

theorem Erdos726.erdos_726.variants.mertens_estimate : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ∑ p ∈ Finset.range (n + 1) with Nat.Prime p, 1 / ↑p) fun (n : ℕ) => Real.log (Real.log ↑n)

The classical estimate of Mertens states that $\sum_{p\leq n}\frac{1}{p}\sim \log\log n$.