Erdős Problem 454

References:

• erdosproblems.com/454
• [Po79] Pomerance, Carl, The prime number graph. Math. Comp. (1979), 399-408.

noncomputable def Erdos454.f (n : ℕ) : ℕ

Define f n to be the minimum of (n + i).nth Prime - (n - i).nth Prime over i < n.

Equations

• Erdos454.f n = ⨅ (i : Fin n), Nat.nth Prime (n + ↑i) + Nat.nth Prime (n - ↑i)

theorem Erdos454.erdos_454 : sorry ↔ Filter.limsup (fun (n : ℕ) => ↑(f n) - 2 * ↑(Nat.nth Prime n)) Filter.atTop = ⊤

Is it true that limsup (fun n => f n - 2 * (n.nth Prime) : ℕ∞) atTop = ⊤?

theorem Erdos454.erdos_454.two_le_limsup : 2 ≤ Filter.limsup (fun (n : ℕ) => ↑(f n) - 2 * ↑(Nat.nth Prime n)) Filter.atTop

limsup (fun n => f n - 2 * (n.nth Prime) : ℕ∞) atTop ≥ 2, and this is proved in [Po79].