Documentation

PrimeNumberTheoremAnd.eSHP

source
theorem eSHP.table_8_prime_gap_test (p g : ℕ) (h : (p, g) ∈ table_8) (htest : p < 30) :
prime_gap_record p g
source
theorem eSHP.table_8_prime_gap (p g : ℕ) (h : (p, g) ∈ table_8) :
prime_gap_record p g
source
theorem eSHP.table_8_prime_gap_complete_test (p g : ℕ) (hp : p ≤ 30) (hrecord : prime_gap_record p g) :
(p, g) ∈ table_8
source
theorem eSHP.table_8_prime_gap_complete (p g : ℕ) (hp : p ≤ 4 * 10 ^ 18) (hrecord : prime_gap_record p g) :
(p, g) ∈ table_8
source
theorem eSHP.exists_prime_gap_record_le (n : ℕ) :
∃ (m : ℕ), nth_prime m ≤ nth_prime n ∧ nth_prime_gap n ≤ nth_prime_gap m ∧ prime_gap_record (nth_prime m) (nth_prime_gap m)
source
theorem eSHP.max_prime_gap (n : ℕ) (hp : nth_prime n ≤ 4 * 10 ^ 18) :
nth_prime_gap n ≤ 1476
source
theorem eSHP.table_9_prime_gap_test (g P : ℕ) (h : (g, P) ∈ table_9) (htest : P < 30) :
first_gap_record g P
source
theorem eSHP.table_9_prime_gap (g P : ℕ) (h : (g, P) ∈ table_9) :
first_gap_record g P
source
theorem eSHP.nth_prime_vals :
nth_prime 0 = 2 ∧ nth_prime 1 = 3 ∧ nth_prime 2 = 5 ∧ nth_prime 3 = 7 ∧ nth_prime 4 = 11 ∧ nth_prime 5 = 13 ∧ nth_prime 6 = 17 ∧ nth_prime 7 = 19 ∧ nth_prime 8 = 23

Values of the first 9 primes (0-indexed).

source
theorem eSHP.first_gap_odd_gt_1 {g : ℕ} (hg : Odd g) (hg1 : 1 < g) :
first_gap g = 0

For any odd number g > 1, the first prime gap of size g is 0 (meaning it doesn't exist).

source
theorem eSHP.first_gap_1 :
first_gap 1 = 2

The first prime gap of size 1 occurs at prime 2.

source
theorem eSHP.first_gap_2 :
first_gap 2 = 3

The first prime gap of size 2 occurs at prime 3.

source
theorem eSHP.first_gap_3 :
first_gap 3 = 0

The first prime gap of size 3 does not occur.

source
theorem eSHP.first_gap_4 :
first_gap 4 = 7

The first prime gap of size 4 occurs at prime 7.

source
theorem eSHP.first_gap_5 :
first_gap 5 = 0

The first prime gap of size 5 does not occur.

source
theorem eSHP.first_gap_6 :
first_gap 6 = 23

The first prime gap of size 6 occurs at prime 23.

source
theorem eSHP.first_gap_7 :
first_gap 7 = 0

The first prime gap of size 7 does not occur.

source
theorem eSHP.table_9_prime_gap_complete_test (g P : ℕ) (hg : g < 8) (hg' : 0 < g) (hrecord : first_gap_record g P) :
(g, P) ∈ table_9
source
theorem eSHP.table_9_prime_gap_complete (g P : ℕ) (hg : g < 1346) (hg' : 0 < g) (hrecord : first_gap_record g P) :
(g, P) ∈ table_9
source
theorem eSHP.exists_prime_gap (g : ℕ) (hg : g ∈ Set.Ico 1 1476) (hg' : Even g ∨ g = 1) :
first_gap g ≤ 3278018069102480227