The exact base range, including prime squares

Below the square of the sieve threshold a rough integer is a unit or a prime. At the square endpoint there is one additional integer precisely when the threshold itself is prime.

theorem LiLiuPrereqBuchstab.rough_prime_iff {z : ℝ} {p : ℕ} (hp : Nat.Prime p) : Rough z p ↔ z ≤ ↑p

theorem LiLiuPrereqBuchstab.sq_le_of_rough_composite {z : ℝ} {n : ℕ} (hz : 0 ≤ z) (hn0 : 0 < n) (hn1 : n ≠ 1) (hnp : ¬Nat.Prime n) (hr : Rough z n) : z ^ 2 ≤ ↑n

theorem LiLiuPrereqBuchstab.rough_composite_at_sq {x z : ℝ} {n : ℕ} (hz : 0 ≤ z) (hx : x ≤ z ^ 2) (hn : n ∈ roughNumbers x z) (hn1 : n ≠ 1) (hnp : ¬Nat.Prime n) : ∃ (p : ℕ), Nat.Prime p ∧ ↑p = z ∧ n = p ^ 2 ∧ x = z ^ 2

theorem LiLiuPrereqBuchstab.rough_below_sq_iff {x z : ℝ} (hz : 0 ≤ z) (hx : x < z ^ 2) {n : ℕ} : n ∈ roughNumbers x z ↔ n = 1 ∧ 1 ≤ x ∨ Nat.Prime n ∧ z ≤ ↑n ∧ ↑n ≤ x

noncomputable def LiLiuPrereqBuchstab.primeNumbers (x z : ℝ) : Finset ℕ

Equations

• LiLiuPrereqBuchstab.primeNumbers x z = Finset.filter Nat.Prime (LiLiuPrereqBuchstab.roughNumbers x z)

@[simp]

theorem LiLiuPrereqBuchstab.mem_primeNumbers {x z : ℝ} {n : ℕ} : n ∈ primeNumbers x z ↔ Nat.Prime n ∧ z ≤ ↑n ∧ ↑n ≤ x

theorem LiLiuPrereqBuchstab.roughCount_below_sq {x z : ℝ} (hz : 0 ≤ z) (hx1 : 1 ≤ x) (hx : x < z ^ 2) : roughCount x z = 1 + (primeNumbers x z).card

This base formula uses actual primes and includes the unit.

theorem LiLiuPrereqBuchstab.roughNumbers_prime_sq {p : ℕ} (hp : Nat.Prime p) : roughNumbers (↑p ^ 2) ↑p = insert 1 (insert (p ^ 2) (primeNumbers (↑p ^ 2) ↑p))

The only nonunit, nonprime rough integer at the square endpoint is p².

theorem LiLiuPrereqBuchstab.roughCount_prime_sq {p : ℕ} (hp : Nat.Prime p) : roughCount (↑p ^ 2) ↑p = 2 + (primeNumbers (↑p ^ 2) ↑p).card

theorem LiLiuPrereqBuchstab.roughCount_le_sq_no_square {x z : ℝ} (hz : 0 ≤ z) (hx1 : 1 ≤ x) (hx : x ≤ z ^ 2) (hnsq : ¬∃ (p : ℕ), Nat.Prime p ∧ ↑p = z ∧ x = z ^ 2) : roughCount x z = 1 + (primeNumbers x z).card

noncomputable def LiLiuPrereqBuchstab.squareCorrection (x z : ℝ) : ℕ

Equations

• LiLiuPrereqBuchstab.squareCorrection x z = if ∃ (p : ℕ), Nat.Prime p ∧ ↑p = z ∧ x = z ^ 2 then 1 else 0

theorem LiLiuPrereqBuchstab.roughCount_le_sq {x z : ℝ} (hz : 0 ≤ z) (hx1 : 1 ≤ x) (hx : x ≤ z ^ 2) : roughCount x z = 1 + (primeNumbers x z).card + squareCorrection x z

Exact formula on the entire closed base range. The final indicator is nonzero only at a prime-square endpoint, not at every square endpoint.

theorem LiLiuPrereqBuchstab.primeNumbers_eq_sdiff {x z : ℝ} (hx : 0 ≤ x) : primeNumbers x z = (⌊x⌋₊ + 1).primesBelow \ ⌈z⌉₊.primesBelow

theorem LiLiuPrereqBuchstab.card_primeNumbers {x z : ℝ} (hx : 0 ≤ x) (hzx : z ≤ x) : (primeNumbers x z).card = ⌊x⌋₊.primeCounting - ⌈z⌉₊.primeCounting'

primeCounting' (ceil z) counts primes strictly below the real cutoff. In particular a prime equal to z is not subtracted.

theorem LiLiuPrereqBuchstab.roughCount_le_sq_primeCounting {x z : ℝ} (hz : 0 ≤ z) (hx1 : 1 ≤ x) (hzx : z ≤ x) (hx : x ≤ z ^ 2) : roughCount x z = 1 + (⌊x⌋₊.primeCounting - ⌈z⌉₊.primeCounting') + squareCorrection x z