Erdős Problem 233

References:

• erdosproblems.com/233
• A074741
• Wikipedia

theorem Erdos233.sum_of_squares_of_prime_gaps_lower_bound : (fun (N : ℕ) => ↑N * Real.log ↑N ^ 2) ≪ fun (N : ℕ) => ∑ n ∈ Finset.range N, ↑(primeGap n) ^ 2

The prime number theorem immediately implies a lower bound of $\gg N(\log N)^2$ for the sum of squares of gaps between consecutive primes.

theorem Erdos233.erdos_233 : (fun (N : ℕ) => ∑ n ∈ Finset.range N, ↑(primeGap n) ^ 2) ≪ fun (N : ℕ) => ↑N * Real.log ↑N ^ 2

A conjecture by Heath-Brown: The sum of squares of the first $N$ gaps between consecutive primes behaves like $N * (log N)^2$.

theorem Erdos233.erdos_233.variant (h : RiemannHypothesis) : (fun (N : ℕ) => ∑ n ∈ Finset.range N, ↑(primeGap n) ^ 2) ≪ fun (N : ℕ) => ↑N * Real.log ↑N ^ 4

Cramér proved an upper bound of $O(N(\log N)^4)$ conditional on the Riemann hypothesis.