Oppermann's Conjecture

Reference: Wikipedia

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 ≥ 2 there exists a prime between x(x-1) and x².

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 ≥ 2 there exists a prime between x² 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 ≥ 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.