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 + 1) - q n ≥ q n - q (n - 1)) →
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 + 1) - q n ≥ q n - q (n - 1). Must lim q n / (n ^ 2) = ∞?
theorem
Erdos455.erdos_455.liminf
(q : ℕ → ℕ)
:
StrictMono q →
(∀ (n : ℕ), Nat.Prime (q n) ∧ q (n + 1) - q n ≥ q n - q (n - 1)) →
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 + 1) - q n ≥ q n - q (n - 1). Then liminf q n / (n ^ 2) > 0.352, and this is proved in
[Ri76].