Oppermann's Conjecture

References:

• Wikipedia
• Luan Alberto Ferreira, Real exponential sums over primes and prime gaps

theorem Oppermann.oppermann_conjecture.parts.i (x : ℕ) (hx : 2 ≤ x) : ∃ p ∈ Finset.Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p

For every integer $x \ge 2$ there exists a prime between $x(x-1)$ and $x^2$.

theorem Oppermann.oppermann_conjecture.parts.ii (x : ℕ) (hx : 2 ≤ x) : ∃ p ∈ Finset.Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p

For every integer $x \ge 2$ there exists a prime between $x^2$ and $x(x+1)$.

theorem Oppermann.oppermann_conjecture (x : ℕ) (hx : 2 ≤ x) : (∃ p ∈ Finset.Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Finset.Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p

Oppermann's Conjecture: For every integer $x \ge 2$, the following hold:

• There exists a prime between $x(x-1)$ and $x^2$.
• There exists a prime between $x^2$ and $x(x+1)$.

theorem Oppermann.oppermann_implies_brocard (n : ℕ) (hn : 1 ≤ n) (P : ∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Finset.Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Finset.Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p) : 4 ≤ (Finset.filter Nat.Prime (Finset.Ioo (Nat.nth Nat.Prime n ^ 2) (Nat.nth Nat.Prime (n + 1) ^ 2))).card

Oppermann's conjecture implies Brocard's conjecture.

theorem Oppermann.oppermann_implies_legendre (n : ℕ) (hn : 1 ≤ n) (P : ∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Finset.Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Finset.Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p) : ∃ p ∈ Finset.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p

Oppermann's conjecture implies Legendre's conjecture.

theorem Oppermann.oppermann_conjecture.ferreira_large_x : ∀ᶠ (x : ℕ) in Filter.atTop, (∃ p ∈ Finset.Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Finset.Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p

Ferreira proved that Oppermann's conjecture is true for sufficiently large x.