Erdős Problem 218

Reference: erdosproblems.com/218

theorem Erdos218.erdos_218.variants.le : {n : ℕ | primeGap n ≤ primeGap (n + 1)}.HasDensity (1 / 2)

The set of indices $n$ for which a prime gap is followed by a larger or equal prime gap has a natural density of $\frac 1 2$.

theorem Erdos218.erdos_218.variants.ge : {n : ℕ | primeGap (n + 1) ≤ primeGap n}.HasDensity (1 / 2)

The set of indices $n$ for which a prime gap is preceeded by a larger or equal prime gap has a natural density of $\frac 1 2$.

theorem Erdos218.erdos_218.variants.infinite_equal_prime_gap : {n : ℕ | primeGap n = primeGap (n + 1)}.Infinite

There are infintely many indices $n$ such that the prime gap at $n$ is equal to the prime gap at $n+1$. This is equivalent to the existence of infinitely many arithmetic progressions of length $3$, see erdos_141.variant.infinite_three.