def Oppermann.InLowerOppermannInterval (n p : ℕ) : Prop

Prime interval below n^2 used in Oppermann's conjecture.

Equations

• Oppermann.InLowerOppermannInterval n p = (n * (n - 1) < p ∧ p < n ^ 2)

def Oppermann.InUpperOppermannInterval (n q : ℕ) : Prop

Prime interval above n^2 used in Oppermann's conjecture.

Equations

• Oppermann.InUpperOppermannInterval n q = (n ^ 2 < q ∧ q < n * (n + 1))

def Oppermann.HasOppermannPrimes (n : ℕ) : Prop

Oppermann witness pair for index n.

Equations

• Oppermann.HasOppermannPrimes n = ∃ (p : ℕ), ∃ (q : ℕ), Nat.Prime p ∧ Nat.Prime q ∧ Oppermann.InLowerOppermannInterval n p ∧ Oppermann.InUpperOppermannInterval n q

def Oppermann.HasPrimeBetweenSquares (n : ℕ) : Prop

One-prime-between-squares predicate used to compare with Legendre.

Equations

• Oppermann.HasPrimeBetweenSquares n = ∃ (p : ℕ), Nat.Prime p ∧ n ^ 2 < p ∧ p < (n + 1) ^ 2

instance Oppermann.instDecidableInLowerOppermannInterval (n p : ℕ) : Decidable (InLowerOppermannInterval n p)

Equations

• Oppermann.instDecidableInLowerOppermannInterval n p = id inferInstance

instance Oppermann.instDecidableInUpperOppermannInterval (n q : ℕ) : Decidable (InUpperOppermannInterval n q)

Equations

• Oppermann.instDecidableInUpperOppermannInterval n q = id inferInstance