Erdős Problem 455

References:

• erdosproblems.com/455
• [Ri76] Richter, Bernd, Über die Monotonie von Differenzenfolgen. Acta Arith. (1976), 225-227.

theorem Erdos455.erdos_455 : sorry ↔ ∀ (q : ℕ → ℕ), StrictMono q → (∀ (n : ℕ), Nat.Prime (q n) ∧ q (n + 2) - q (n + 1) ≥ q (n + 1) - q n) → Filter.Tendsto (fun (n : ℕ) => ↑(q n) / ↑n ^ 2) Filter.atTop Filter.atTop

Let q : ℕ → ℕ be a strictly increasing sequence of primes such that q (n + 2) - q (n + 1) ≥ q (n + 1) - q n. Must lim q n / (n ^ 2) = ∞?

theorem Erdos455.erdos_455.liminf (q : ℕ → ℕ) : StrictMono q → (∀ (n : ℕ), Nat.Prime (q n) ∧ q (n + 2) - q (n + 1) ≥ q (n + 1) - q n) → Filter.liminf (fun (n : ℕ) => ↑(q n) / ↑n ^ 2) Filter.atTop > 0.352

Let q : ℕ → ℕ be a strictly increasing sequence of primes such that q (n + 2) - q (n + 1) ≥ q (n + 1) - q n. Then liminf q n / (n ^ 2) > 0.352, and this is proved in [Ri76].