Erdős Problem 950

References:

• erdosproblems.com/855
• erdosproblems.com/950
• [Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72.
• mathoverflow/508491

noncomputable def Erdos950.f (n : ℕ) : ℝ

Let $f(n) = \sum_{p<n}\frac{1}{n-p}$.

Equations

• Erdos950.f n = ∑ p ∈ Finset.range n with Prime p, 1 / (↑n - ↑p)

theorem Erdos950.erdos_950.parts.i : sorry ↔ Filter.liminf (fun (n : ℕ) => ↑(f n)) Filter.atTop = 1

Is it true that $\liminf f(n)=1$?

theorem Erdos950.erdos_950.parts.ii : sorry ↔ Filter.limsup (fun (n : ℕ) => ↑(f n)) Filter.atTop = ⊤

Is it true that $\limsup f(n)=\infty$?

theorem Erdos950.erdos_950.parts.iii : sorry ↔ f =o[Filter.atTop] fun (n : ℕ) => Real.log (Real.log ↑n)

Is it true that $f(n)=o(\log\log n)$ for all $n$?

theorem Erdos950.erdos_950.variants.debruijn_erdos_turan : (Asymptotics.IsEquivalent Filter.atTop (fun (x : ℕ) => ∑ n ∈ Finset.range x, f n) fun (x : ℕ) => ↑x) ∧ Asymptotics.IsEquivalent Filter.atTop (fun (x : ℕ) => ∑ n ∈ Finset.range x, f n ^ 2) fun (x : ℕ) => ↑x

This function was considered by de Bruijn, Erdős, and Turán, who showed that $\sum_{n<x}f(n)\sim \sum_{n<x}f(n)^2\sim x$. They gave no proofs, but a proof of the (harder) second claim is given by Gorodetsky here [mathoverflow/508491].

theorem Erdos950.erdos_950.variants.weaker_pi : sorry ↔ ∀ ε > 0, ∀ᶠ (x : ℕ) in Filter.atTop, ∃ y < x, ↑x.primeCounting < ↑y.primeCounting + ε * ↑(x - y).primeCounting

Erdős writes that a 'weaker conjecture which is perhaps not quite inaccessible' is that, for every $\epsilon>0$, if $x$ is sufficiently large there exists $y<x$ such that $\pi(x)< \pi(y)+\epsilon \pi(x-y)$. Compare this to [855].

theorem Erdos950.erdos_950.variants.weaker_pi_implies_f (h : ∃ C > 0, ∃ K > 0, ∀ᶠ (x : ℕ) in Filter.atTop, ∀ (y : ℕ), ↑y < ↑x - Real.log ↑x ^ C → ↑x.primeCounting < ↑y.primeCounting + K * ((↑x - ↑y) / Real.log ↑x)) : f =O[Filter.atTop] fun (n : ℕ) => Real.log (Real.log (Real.log ↑n))

He notes that if $\pi(x)< \pi(y)+O\left(\frac{x-y}{\log x}\right)$ for all $y<x-(\log x)^C$ for some constant $C>0$ then $f(n)\ll \log\log\log n$.

theorem Erdos950.erdos_950.variants.sum_primes : sorry ↔ Asymptotics.IsEquivalent Filter.atTop (fun (x : ℕ) => ∑ p ∈ Finset.range x with Prime p, f p ^ 2) fun (x : ℕ) => ↑x.primeCounting

The study of $f(p)$ is even harder, and Erdős could not prove that $\sum_{p<x}f(p)^2\sim \pi(x)$.