Depth stabilisation of Rosser's sieve ([I71, pp. 23, 26])

A failing tuple p₁ > ⋯ > p_l of depth l ≥ 3 passed the test at index l - 2, so p₁ ⋯ p_{l-1} < p₁ ⋯ p_{l-2} p_{l-2}² < y; an element d = p₁ ⋯ p_l of rosserSet lower y z satisfies d < y as soon as l ≥ 2 (or l ≥ 1 for the upper sieve). Hence if every product of r distinct primes below z is at least y (LeProdPrimesLT r y z), the recursion stops at depth r:

• fail_add_eq: 2 ≤ r → LeProdPrimesLT r y z → fail lower (r + j) y z = fail lower r y z;
• card_filter_rosserSet_add_eq: 1 ≤ r → LeProdPrimesLT (r + 1) y z → #{d ∈ D | ω(d) ≤ r + j} = #{d ∈ D | ω(d) ≤ r}.

Products of r distinct primes are at least (r + 1)! (factorial_card_add_one_le_prod), and (r + 1)! ≥ y once r + 2 > 2 log y / log log y and y is large (exists_le_factorial), which gives [I71]'s "if m + 1 > 2 log y / log log y then Q_{m+1, y} = Q_{m-1, y}" (exists_fail_add_eq, exists_card_filter_rosserSet_add_eq).

def IwaniecLinearSieve.LeProdPrimesLT (r : ℕ) (y z : ℝ) : Prop

y is at most every product of r distinct primes below z (vacuous if there are fewer than r such primes).

Equations

• IwaniecLinearSieve.LeProdPrimesLT r y z = ∀ T ⊆ IwaniecLinearSieve.primesLT z, T.card = r → y ≤ ∏ p ∈ T, ↑p

theorem IwaniecLinearSieve.one_le_prod_primes {T : Finset ℕ} {z : ℝ} (hT : T ⊆ primesLT z) : 1 ≤ ∏ p ∈ T, ↑p

theorem IwaniecLinearSieve.LeProdPrimesLT.div {r : ℕ} {y z : ℝ} {p : ℕ} (h : LeProdPrimesLT (r + 1) y z) (hp : p ∈ primesLT z) : LeProdPrimesLT r (y / ↑p) ↑p

One level down the recursion.

theorem IwaniecLinearSieve.LeProdPrimesLT.succ {r : ℕ} {y z : ℝ} (h : LeProdPrimesLT r y z) : LeProdPrimesLT (r + 1) y z

theorem IwaniecLinearSieve.LeProdPrimesLT.mono {r : ℕ} {y z : ℝ} {s : ℕ} (h : LeProdPrimesLT r y z) (hrs : r ≤ s) : LeProdPrimesLT s y z

theorem IwaniecLinearSieve.factorial_card_add_one_le_prod (T : Finset ℕ) (hT : ∀ n ∈ T, 2 ≤ n) : (T.card + 1).factorial ≤ ∏ n ∈ T, n

A product of #T distinct integers ≥ 2 is at least (#T + 1)!.

theorem IwaniecLinearSieve.leProdPrimesLT_of_le_factorial {r : ℕ} {y z : ℝ} (h : y ≤ ↑(r + 1).factorial) : LeProdPrimesLT r y z

Stabilisation of fail

theorem IwaniecLinearSieve.fail_succ_congr {lower : Bool} {y z : ℝ} {a b : ℕ} (h : ∀ p ∈ rosserPrimes lower y z, fail (!lower) a (y / ↑p) ↑p = fail (!lower) b (y / ↑p) ↑p) : fail lower (a + 1) y z = fail lower (b + 1) y z

theorem IwaniecLinearSieve.fail_add_eq {lower : Bool} {r : ℕ} {y z : ℝ} (hr : 2 ≤ r) (h : LeProdPrimesLT r y z) (j : ℕ) : fail lower (r + j) y z = fail lower r y z

If every product of r ≥ 2 distinct primes below z is at least y, the deficits do not change beyond depth r.

theorem IwaniecLinearSieve.fail_add_eq_of_le_factorial {lower : Bool} {r : ℕ} {y z : ℝ} (hr : 2 ≤ r) (h : y ≤ ↑(r + 1).factorial) (j : ℕ) : fail lower (r + j) y z = fail lower r y z

Stabilisation of the depth-truncated counts

theorem IwaniecLinearSieve.lt_of_mem_rosserSet {lower : Bool} {y z : ℝ} {d : ℕ} (hd : d ∈ rosserSet lower y z) (hω : (if lower = true then 2 else 1) ≤ d.primeFactors.card) : ↑d < y

Elements of rosserSet lower y z with at least two prime factors (at least one for the upper sieve) are smaller than y.

theorem IwaniecLinearSieve.card_primeFactors_le_of_mem_rosserSet {lower : Bool} {r : ℕ} {y z : ℝ} {d : ℕ} (hr : 1 ≤ r) (h : LeProdPrimesLT (r + 1) y z) (hd : d ∈ rosserSet lower y z) : d.primeFactors.card ≤ r

If every product of r + 1 ≥ 2 distinct primes below z is at least y, no element of rosserSet lower y z has more than r prime factors.

theorem IwaniecLinearSieve.card_filter_rosserSet_add_eq {lower : Bool} {r : ℕ} {y z : ℝ} (hr : 1 ≤ r) (h : LeProdPrimesLT (r + 1) y z) (j : ℕ) : {d ∈ rosserSet lower y z | d.primeFactors.card ≤ r + j}.card = {d ∈ rosserSet lower y z | d.primeFactors.card ≤ r}.card

The numerical form

theorem IwaniecLinearSieve.mul_log_sub_one_le_log_factorial (n : ℕ) : ↑n * (Real.log ↑n - 1) ≤ Real.log ↑n.factorial

n (log n - 1) ≤ log n!.

theorem IwaniecLinearSieve.log_le_two_mul_sqrt {x : ℝ} (hx : 0 ≤ x) : Real.log x ≤ 2 * √x

log x ≤ 2 √x.

theorem IwaniecLinearSieve.exists_le_factorial : ∃ (y₀ : ℝ), ∀ y ≥ y₀, ∀ (r : ℕ), 2 * Real.log y / Real.log (Real.log y) < ↑r + 2 → 2 ≤ r ∧ y ≤ ↑(r + 1).factorial

[I71, p. 23]: if r + 2 > 2 log y / log log y and y is large then y ≤ (r + 1)!, so every product of r distinct primes is at least y; moreover r ≥ 2.

theorem IwaniecLinearSieve.exists_fail_add_eq : ∃ (y₀ : ℝ), ∀ y ≥ y₀, ∀ (lower : Bool) (r : ℕ) (z : ℝ), 2 * Real.log y / Real.log (Real.log y) < ↑r + 2 → ∀ (j : ℕ), fail lower (r + j) y z = fail lower r y z

[I71, p. 23]: for y ≥ y₀ and r + 2 > 2 log y / log log y, the deficits do not change beyond depth r.

theorem IwaniecLinearSieve.exists_card_filter_rosserSet_add_eq : ∃ (y₀ : ℝ), ∀ y ≥ y₀, ∀ (lower : Bool) (r : ℕ) (z : ℝ), 2 * Real.log y / Real.log (Real.log y) < ↑r + 2 → ∀ (j : ℕ), {d ∈ rosserSet lower y z | d.primeFactors.card ≤ r - 1 + j}.card = {d ∈ rosserSet lower y z | d.primeFactors.card ≤ r - 1}.card

[I71, p. 26]: for y ≥ y₀ and r + 2 > 2 log y / log log y, no element of rosserSet lower y z has more than r - 1 prime factors; in particular the depth-truncated counts do not change beyond depth r.