[I71, Corollaries 1 and 3 to Lemma 13]

With L = log y and t_p = L / log p, so that the inner level of the recursion at p is (y/p, p) with parameter t_p - 1 (log (y/p) = log p · (t_p - 1)).

• lemma13_param: Lemma 13 in the variable t = L / log u: for F ≥ 0 antitone on [α, β], |∑_{y^{1/β} ≤ p ≤ y^{1/α}} F(t_p)/p - ∫_α^β F(t)/t dt| ≤ C F(α) pntE(y^{1/β}) (substitution u = e^{L/t} in lemma13_mono_of_subset).
• cor1: Corollary 1, for the primes y^{1/β} ≤ p < y^{1/α} and any M ≥ 0 antitone on [α - 1, β - 1].
• cor3: Corollary 3, for the primes y^{1/b} ≤ p in rosserPrimes lower y (y^{1/s}) (the primes of the recursion), uniformly in sMin lower ≤ s, with s₀ = e^{32} and the upper limit ξ replaced by any b ≥ s₀ with 160 b² log⁴ b ≤ L² and y^{1/b} ≥ 2.

Lemma 13 in the variable t = log y / log u

theorem IwaniecLinearSieve.integral_comp_log_div {F : ℝ → ℝ} {y α β : ℝ} (hy : 1 < y) (hα : 0 < α) (hαβ : α ≤ β) : ∫ (u : ℝ) in y ^ (1 / β)..y ^ (1 / α), F (Real.log y / Real.log u) / (u * Real.log u) = ∫ (t : ℝ) in α..β, F t / t

theorem IwaniecLinearSieve.log_rpow_one_div {y : ℝ} (hy : 0 < y) (γ : ℝ) : Real.log (y ^ (1 / γ)) = Real.log y / γ

theorem IwaniecLinearSieve.div_log_mem_Icc {y α β u : ℝ} (hy : 1 < y) (hα : 0 < α) (hαβ : α ≤ β) (hu : u ∈ Set.Icc (y ^ (1 / β)) (y ^ (1 / α))) : 0 < Real.log u ∧ Real.log y / Real.log u ∈ Set.Icc α β

For u ∈ [y^{1/β}, y^{1/α}], log y / log u ∈ [α, β].

theorem IwaniecLinearSieve.lemma13_param : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (F : ℝ → ℝ) (y α β : ℝ) (S : Finset ℕ), 1 < y → 0 < α → α ≤ β → 2 ≤ y ^ (1 / β) → AntitoneOn F (Set.Icc α β) → (∀ t ∈ Set.Icc α β, 0 ≤ F t) → (∀ p ∈ S, Nat.Prime p ∧ y ^ (1 / β) ≤ ↑p ∧ ↑p ≤ y ^ (1 / α)) → (∀ (p : ℕ), Nat.Prime p → y ^ (1 / β) < ↑p → ↑p < y ^ (1 / α) → p ∈ S) → |∑ p ∈ S, F (Real.log y / Real.log ↑p) / ↑p - ∫ (t : ℝ) in α..β, F t / t| ≤ C * F α * pntE (y ^ (1 / β))

[I71, Lemma 13] in the variable t = log y / log u: for F ≥ 0 antitone on [α, β], and any set S of primes between those in (y^{1/β}, y^{1/α}) and those in [y^{1/β}, y^{1/α}], |∑_{p ∈ S} F(t_p)/p - ∫_α^β F(t)/t dt| ≤ C F(α) pntE(y^{1/β}).

Corollary 1

theorem IwaniecLinearSieve.log_div_prime_eq {y : ℝ} {p : ℕ} (hy : 0 < y) (hp : 1 < p) : Real.log (y / ↑p) = Real.log ↑p * (Real.log y / Real.log ↑p - 1)

theorem IwaniecLinearSieve.le_div_log_of_le_rpow {y α : ℝ} {p : ℕ} (hy : 1 < y) (hα : 0 < α) (hp : 1 < p) (hpA : ↑p ≤ y ^ (1 / α)) : α ≤ Real.log y / Real.log ↑p

log y / log p ≥ α for p ≤ y^{1/α}.

theorem IwaniecLinearSieve.antitoneOn_div_sub_one : AntitoneOn (fun (t : ℝ) => t / (t - 1)) (Set.Ioi 1)

theorem IwaniecLinearSieve.cor1 : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (M : ℝ → ℝ) (y α β : ℝ), 1 < y → 2 ≤ α → α ≤ β → 2 ≤ y ^ (1 / β) → AntitoneOn M (Set.Icc (α - 1) (β - 1)) → (∀ t ∈ Set.Icc (α - 1) (β - 1), 0 ≤ M t) → |∑ p ∈ primesLT (y ^ (1 / α)) with y ^ (1 / β) ≤ ↑p, M (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p)) - (∫ (t : ℝ) in α..β, M (t - 1) / (t - 1)) / Real.log y| ≤ C * M (α - 1) * pntE (y ^ (1 / β)) / Real.log y

[I71, Corollary 1 to Lemma 13]: for M ≥ 0 antitone on [α - 1, β - 1], 2 ≤ α ≤ β, y^{1/β} ≥ 2, |∑_{y^{1/β} ≤ p < y^{1/α}} M(t_p - 1)/(p log (y/p)) - L⁻¹ ∫_α^β M(t-1)/(t-1) dt| ≤ C M(α - 1) pntE(y^{1/β}) / L.

theorem IwaniecLinearSieve.cor1_le : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (M : ℝ → ℝ) (y α β : ℝ), 1 < y → 2 ≤ α → α ≤ β → 2 ≤ y ^ (1 / β) → AntitoneOn M (Set.Icc (α - 1) (β - 1)) → (∀ t ∈ Set.Icc (α - 1) (β - 1), 0 ≤ M t) → ∑ p ∈ primesLT (y ^ (1 / α)) with y ^ (1 / β) ≤ ↑p, M (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p)) ≤ (∫ (t : ℝ) in α..β, M (t - 1) / (t - 1)) / Real.log y + C * M (α - 1) * pntE (y ^ (1 / β)) / Real.log y

[I71, Corollary 1 to Lemma 13], one-sided form.

Corollary 3

theorem IwaniecLinearSieve.errMaj_shift_sq_le (lower lower' : Bool) {s : ℝ} (hs : 2 ≤ s) : errMaj lower' (s - 1) * (s ^ 2 / (s - 1) ^ 2) ≤ 32 * s ^ 2 * errMaj lower s

G'(s-1) s²/(s-1)² ≤ 32 s² G(s) for s ≥ 2 (Lemma 8 and the Corollary to Lemma 6).

theorem IwaniecLinearSieve.growth_le_delta {y t a : ℝ} (ht : 1 ≤ t) (hta : t ≤ a) : (1 + t ^ 2 * Real.log t ^ 5 / Real.log y ^ 2) ^ (5 * (t - 1)) ≤ delta a y

(1 + t² log⁵ t / L²)^{5(t-1)} ≤ δ(a, y) for 1 ≤ t ≤ a.

theorem IwaniecLinearSieve.cor3_summand_le {G : ℝ → ℝ} {y : ℝ} {p : ℕ} (hy : 1 < y) (hp : 1 < p) (ht : 2 ≤ Real.log y / Real.log ↑p) (hG : 0 ≤ G (Real.log y / Real.log ↑p - 1)) : delta (Real.log y / Real.log ↑p - 1) (y / ↑p) * G (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p) ^ 2) ≤ (1 + (Real.log y / Real.log ↑p) ^ 2 * Real.log (Real.log y / Real.log ↑p) ^ 5 / Real.log y ^ 2) ^ (5 * (Real.log y / Real.log ↑p - 1)) * G (Real.log y / Real.log ↑p - 1) * ((Real.log y / Real.log ↑p) ^ 2 / (Real.log y / Real.log ↑p - 1) ^ 2) / Real.log y ^ 2 / ↑p

The summand of Corollary 3: with t = t_p ≥ 2, log (y/p) = L (t-1)/t, so δ(t - 1, y/p) G(t-1) / (p log² (y/p)) ≤ (1 + t² log⁵ t / L²)^{5(t-1)} G(t-1) (t²/(t-1)²) / L² / p.

theorem IwaniecLinearSieve.errMaj_not_eq_majG (lower : Bool) : (errMaj !lower) = majG (if lower = true then 1 else 0)

theorem IwaniecLinearSieve.errMaj_eq_majG_succ (lower : Bool) : errMaj lower = majG ((if lower = true then 1 else 0) + 1)

theorem IwaniecLinearSieve.cor3_large : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (lower : Bool) (y s b : ℝ) (S : Finset ℕ), 1 < y → Real.exp 32 ≤ s → s ≤ b → 2 ≤ y ^ (1 / b) → b ^ 2 * Real.log b ^ 4 ≤ Real.log y ^ 2 / 160 → (∀ p ∈ S, Nat.Prime p ∧ y ^ (1 / b) ≤ ↑p ∧ ↑p ≤ y ^ (1 / s)) → (∀ (p : ℕ), Nat.Prime p → y ^ (1 / b) < ↑p → ↑p < y ^ (1 / s) → p ∈ S) → ∑ p ∈ S, delta (Real.log y / Real.log ↑p - 1) (y / ↑p) * errMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p) ^ 2) ≤ delta s y * errMaj lower s / Real.log y ^ 2 * (1 + C * b ^ 2 * pntE (y ^ (1 / b)))

Corollary 3 on [s, b] with e^{32} ≤ s (Lemmas 11, 12 and 13). S is any set of primes between those in (y^{1/b}, y^{1/s}) and those in [y^{1/b}, y^{1/s}].

theorem IwaniecLinearSieve.cor3_small : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (lower : Bool) (y s a : ℝ) (S : Finset ℕ), 1 < y → errLower lower ≤ s → s ≤ a → a ≤ Real.exp 32 → 2 ≤ y ^ (1 / a) → (∀ p ∈ S, Nat.Prime p ∧ y ^ (1 / a) ≤ ↑p ∧ ↑p ≤ y ^ (1 / s)) → (∀ (p : ℕ), Nat.Prime p → y ^ (1 / a) < ↑p → ↑p < y ^ (1 / s) → p ∈ S) → ∑ p ∈ S, delta (Real.log y / Real.log ↑p - 1) (y / ↑p) * errMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p) ^ 2) ≤ delta (Real.exp 32) y / Real.log y ^ 2 * (errMaj lower s - errMaj lower a + C * s ^ 2 * errMaj lower s * pntE (y ^ (1 / a)))

Corollary 3 on [s, a] with a ≤ e^{32}: here δ(t_p - 1, y/p) ≤ δ(e^{32}, y) and Lemma 13 is applied to G'(t-1) t²/(t-1)² directly.

theorem IwaniecLinearSieve.rpow_one_div_le_rpow_one_div {y u v : ℝ} (hy : 1 ≤ y) (hu : 0 < u) (huv : u ≤ v) : y ^ (1 / v) ≤ y ^ (1 / u)

theorem IwaniecLinearSieve.cor3_primesLT : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (lower : Bool) (y s b : ℝ), 1 < y → errLower lower ≤ s → Real.exp 32 ≤ b → 2 ≤ y ^ (1 / b) → b ^ 2 * Real.log b ^ 4 ≤ Real.log y ^ 2 / 160 → ∑ p ∈ primesLT (y ^ (1 / s)) with y ^ (1 / b) ≤ ↑p, delta (Real.log y / Real.log ↑p - 1) (y / ↑p) * errMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p) ^ 2) ≤ delta (max s (Real.exp 32)) y * errMaj lower s / Real.log y ^ 2 * (1 + C * b ^ 2 * pntE (y ^ (1 / b)))

[I71, Corollary 3 to Lemma 13] for the primes y^{1/b} ≤ p < y^{1/s}, errLower lower ≤ s (so s ≥ 2, and s ≥ 3 for the upper sieve, where (3.13) holds).

theorem IwaniecLinearSieve.lt_rpow_one_div_max_three {y s x : ℝ} (hy : 1 < y) (hs : 0 < s) (hx : 0 ≤ x) : x < y ^ (1 / max s 3) ↔ x < y ^ (1 / s) ∧ x ^ 3 < y

p < y^{1/max s 3} ↔ p < y^{1/s} ∧ p³ < y (for y > 1, s > 0, p ≥ 0).

theorem IwaniecLinearSieve.cor3 : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (lower : Bool) (y s b : ℝ), 1 < y → sMin lower ≤ s → Real.exp 32 ≤ b → 2 ≤ y ^ (1 / b) → b ^ 2 * Real.log b ^ 4 ≤ Real.log y ^ 2 / 160 → ∑ p ∈ rosserPrimes lower y (y ^ (1 / s)) with y ^ (1 / b) ≤ ↑p, delta (Real.log y / Real.log ↑p - 1) (y / ↑p) * errMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p) ^ 2) ≤ delta (max s (Real.exp 32)) y * errMaj lower s / Real.log y ^ 2 * (1 + C * b ^ 2 * pntE (y ^ (1 / b)))

[I71, Corollary 3 to Lemma 13], for the primes of the Rosser recursion: with t_p = log y / log p, s₀ = e^{32}, sMin lower ≤ s, any b ≥ s₀ with y^{1/b} ≥ 2 and 160 b² log⁴ b ≤ log² y (e.g. b = ξ(y) for large y, exists_xi_large),

∑_{p ∈ rosserPrimes lower y (y^{1/s}), p ≥ y^{1/b}} δ(t_p - 1, y/p) G(!lower)(t_p - 1) / (p log² (y/p)) ≤ δ(max s s₀, y) G(lower)(s) / L² · (1 + C b² pntE(y^{1/b})).

For the upper sieve and s < 3 the primes are those < y^{1/3} and 𝔉(s) = 𝔉(3) = 1, so this reduces to s = 3.

theorem IwaniecLinearSieve.sq_mul_log_pow_four_le_of_le {b b' X : ℝ} (hb : 1 ≤ b) (hbb' : b ≤ b') (h : b' ^ 2 * Real.log b' ^ 4 ≤ X) : b ^ 2 * Real.log b ^ 4 ≤ X

The hypothesis 160 b² log⁴ b ≤ L² passes to smaller b ≥ 1.

theorem IwaniecLinearSieve.cor3_xi : ∃ (C : ℝ) (y₀ : ℝ), 0 ≤ C ∧ ∀ (lower : Bool) (y s : ℝ), y₀ ≤ y → sMin lower ≤ s → ∑ p ∈ rosserPrimes lower y (y ^ (1 / s)) with y ^ (1 / xi y) ≤ ↑p, delta (Real.log y / Real.log ↑p - 1) (y / ↑p) * errMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p) ^ 2) ≤ delta (max s (Real.exp 32)) y * errMaj lower s / Real.log y ^ 2 * (1 + C * xi y ^ 2 * pntE (y ^ (1 / xi y)))

Corollary 3 with b = ξ(y), for y ≥ y₀.