Counting lemmas for [I71, Theorem 5]

• card_rosserSet_le: #(rosserSet lower y y^{1/s}) ≤ y for y > 1, s ≥ 1 (all elements are < y); this is the small-y case.
• card_filter_succ_le: Lemma 17 split at a level w: the primes p < w give at most #(rosserSet lower y w).
• card_rosserSet_rpow_le: the crude count of rosserSet lower y w for w = y^{1/(ξ-1)} ([I71, p. 27]): elements with at most K ≈ ξ(1 - 2/λ) prime factors are counted by π(w)^l / l!, the others by card_filter_le_tail.
• exists_card_small: for large y and sMin lower ≤ s ≤ ξ, 1 + #(rosserSet lower y y^{1/(ξ-1)}) ≤ δ(s, y) G(s) y / (8 L⁴).

theorem IwaniecLinearSieve.TheoremFive.lt_of_mem_rosserSet_rpow {lower : Bool} {y s : ℝ} (hy : 1 < y) (hs : 1 ≤ s) {d : ℕ} (hd : d ∈ rosserSet lower y (y ^ (1 / s))) : ↑d < y

For y > 1 and s ≥ 1, every element of rosserSet lower y y^{1/s} is < y.

theorem IwaniecLinearSieve.TheoremFive.card_rosserSet_le {lower : Bool} {y s : ℝ} (hy : 1 < y) (hs : 1 ≤ s) : ↑(rosserSet lower y (y ^ (1 / s))).card ≤ y

The small-y case: #(rosserSet lower y y^{1/s}) ≤ y for y > 1, s ≥ 1.

theorem IwaniecLinearSieve.TheoremFive.card_filter_succ_le (n : ℕ) (lower : Bool) (y z w : ℝ) : ↑{d ∈ rosserSet lower y z | d.primeFactors.card ≤ n + 1}.card ≤ ↑(rosserSet lower y w).card + ∑ p ∈ rosserPrimes lower y z with w ≤ ↑p, ↑{d ∈ rosserSet (!lower) (y / ↑p) ↑p | d.primeFactors.card ≤ n}.card

Lemma 17 split at w: the primes p < w contribute (with the 1) at most #(rosserSet lower y w).

theorem IwaniecLinearSieve.TheoremFive.card_primesLT_le {w : ℝ} (hw : 0 ≤ w) : ↑(primesLT w).card ≤ w + 1

theorem IwaniecLinearSieve.TheoremFive.card_filter_le_le (lower : Bool) (y : ℝ) {w : ℝ} (hw : 1 ≤ w) (K : ℕ) : ↑{d ∈ rosserSet lower y w | d.primeFactors.card ≤ K}.card ≤ (↑K + 1) * (2 * w) ^ K

Elements with at most K prime factors: at most (K + 1) (2w)^K of them (w ≥ 1).

theorem IwaniecLinearSieve.TheoremFive.count_cutoff_ratio_le {ξ m : ℝ} (hm : 0 < m) (hξ : 1 < ξ) (hmξ : m ≤ ξ) : ξ * (1 - 2 / m) / (ξ - 1) ≤ 1 - 1 / m

The cutoff u = ξ(1 - 2/λ) leaves a saving of 1/λ in the exponent of w.

theorem IwaniecLinearSieve.TheoremFive.mul_log_count_cutoff_ge {ξ m : ℝ} (hm : 2 < m) (hξ : 0 < ξ) (hlogξ : Real.log ξ ≤ m) : ξ * Real.log ξ - 3 * ξ ≤ ξ * (1 - 2 / m) * Real.log (ξ * (1 - 2 / m))

Replacing ξ by the cutoff u = ξ(1 - 2/λ) loses at most 3ξ in u log u.

theorem IwaniecLinearSieve.TheoremFive.card_rosserSet_rpow_le {lower : Bool} {y : ℝ} (hy : 1 < y) (hw : 2 ≤ y ^ (1 / (xi y - 1))) (hSLT : SLT (y ^ (1 / (xi y - 1))) ≤ 2 * lam y) (hlam : 100 ≤ lam y) (h24 : 24 * lam y ≤ xi y) (hlogξ : Real.log (xi y) ≤ lam y) : ↑(rosserSet lower y (y ^ (1 / (xi y - 1)))).card ≤ Real.exp (Real.log y + 2 * xi y - Real.log y / lam y) + 2 * Real.exp (Real.log y - xi y * Real.log (xi y) + xi y * Real.log (lam y) + 5 * xi y)

The crude count of rosserSet lower y w for w = y^{1/(ξ-1)}, ξ = xi y, λ = lam y ([I71, p. 27]): #(rosserSet lower y w) ≤ e^{L + 2ξ - L/λ} + 2 e^{L - ξ log ξ + ξ log λ + 5ξ}.

The comparison (4.9), (4.10)

theorem IwaniecLinearSieve.TheoremFive.one_le_of_sMin_le {lower : Bool} {s : ℝ} (hs : sMin lower ≤ s) : 1 ≤ s

theorem IwaniecLinearSieve.TheoremFive.one_le_delta {s : ℝ} (hs : 1 ≤ s) (y : ℝ) : 1 ≤ delta s y

theorem IwaniecLinearSieve.TheoremFive.exp_le_delta_of_half_le {y s : ℝ} (hy : 1 < y) (hs : xi y / 2 ≤ s) (hlogs : lam y / 2 ≤ Real.log s) : Real.exp (s * (3 * Real.log (lam y) - 5 * Real.log 128)) ≤ delta s y

For s ≥ ξ/2 and log s ≥ λ/2, the growth of δ supplies the factor exp (s (3 log λ - 5 log 128)) in [I71, (4.10)].

theorem IwaniecLinearSieve.TheoremFive.exp_le_delta_errMaj {y s cG : ℝ} (hcG : 0 ≤ cG) (hG : ∀ (r : ℕ) (s : ℝ), 3 ≤ s → Real.exp (-(s * Real.log s) - s * Real.log (Real.log s) - cG * s) ≤ majG r s) (hy : 1 < y) (h2 : 2 * (cG + 5 * Real.log 128) ≤ Real.log (lam y)) (h6 : 6 ≤ xi y) (h8 : lam y / 2 ≤ Real.log (xi y / 2)) (h9 : 4 * Real.log (lam y) + cG ≤ Real.log (xi y)) (h10 : Real.log (xi y) ≤ lam y) (lower : Bool) (hs : sMin lower ≤ s) (hsξ : s ≤ xi y) : Real.exp (-(xi y * Real.log (xi y)) + 3 / 2 * xi y * Real.log (lam y)) ≤ delta s y * errMaj lower s

[I71, (4.9), (4.10)] in the form needed for Theorem 5: for sMin lower ≤ s ≤ ξ, exp(-ξ log ξ + (3/2) ξ log λ) ≤ δ(s, y) G(s), given the lower bound of Lemma 9 with constant c_G ≥ 0 and the scalar facts of eventually_scalar. For s ≤ ξ/2 this uses Lemma 9 only; for s > ξ/2 it uses δ(s, y) ≥ (s² log⁵ s / L²)^{5s} ≥ λ^{3s} 128^{-5s}.

theorem IwaniecLinearSieve.TheoremFive.exists_card_small : ∃ (y₀ : ℝ), ∀ y ≥ y₀, ∀ (lower : Bool) (s : ℝ), sMin lower ≤ s → s ≤ xi y → 1 + ↑(rosserSet lower y (y ^ (1 / (xi y - 1)))).card ≤ delta s y * errMaj lower s * y / (8 * Real.log y ^ 4)

[I71, p. 27]: for large y, sMin lower ≤ s ≤ ξ and w = y^{1/(ξ - 1)}, 1 + #(rosserSet lower y w) ≤ δ(s, y) G(s) y / (8 L⁴).