Oppermann's conjecture

DefinitionPrimes in the lower Oppermann interval#✓fully proved

For a natural number \(n\), this is the number of primes \(p\) with \(n^2 - n \le p \le n^2\).

def oppermannLowerPrimeCount (n : ℕ) : ℕ :=
  ((Finset.Icc (n ^ 2 - n) (n ^ 2)).filter Nat.Prime).card

DefinitionPrimes in the upper Oppermann interval#✓fully proved

For a natural number \(n\), this is the number of primes \(p\) with \(n^2 \le p \le n^2 + n\).

def oppermannUpperPrimeCount (n : ℕ) : ℕ :=
  ((Finset.Icc (n ^ 2) (n ^ 2 + n)).filter Nat.Prime).card

DefinitionMain term for the Oppermann prime counts#✓fully proved

For a natural number \(n\), this is the real number \(n / (2 \log n)\), where \(\log\) is the natural logarithm. It is used as the asymptotic main term for the number of primes in each of the intervals \([n^2 - n, n^2]\) and \([n^2, n^2 + n]\).

For \(n \le 1\) we have \(\log n = 0\), and the value is \(0\) by the convention that division by zero gives zero; this does not affect the asymptotics.

noncomputable def oppermannAsymptotic (n : ℕ) : ℝ :=
  (n : ℝ) / (2 * Real.log n)

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.