[I71, Lemmas 11 and 12]

Write L = log y, x(t) = t² log⁵ t / L², w(t) = t² log⁴ t / L² and A_a(t) = (1 + x(t))^{5(t - a)} (so δ(t, y) = A_0(t)). The logarithmic derivative of A_a is E_a(t) = 5 log (1 + x) + 5 (t - a) x'/(1 + x) ≤ w (15 log t + 25) (rate_bound). With the Corollary to Lemma 10 (c₃ = 4), G_{r+1}(t) log t < 4 G_r(t-1) t/(t-1)², this gives, for log t ≥ 32 and 160 w(t) ≤ 1:

• lemma11: ∫_s^b A_1(t) G_r(t-1) t/(t-1)² dt < δ(s) G_{r+1}(s) for e^{32} ≤ s ≤ b with 160 b² log⁴ b ≤ L² ([I71, (3.15)]; [I71] has s₀ = e^{(120 c₃)^{5/2}} and the condition 100 c₃ ξ² log⁴ ξ < L²);
• lemma12: A_1(t) G_{r+1}(t) is antitone on [s, b];
• antitoneOn_cor3Weight: A_1(t) G_r(t-1) t²/(t-1)² is antitone on [s, b] (this is the monotonicity of b(x) in the proof of [I71, Corollary 3]; [I71] refers to Lemma 12 for it).

Finally exists_xi_large: for large y, ξ(y) ≥ e^{32}, 160 ξ² log⁴ ξ ≤ L² and y^{1/ξ} ≥ 2, via xi_sq_mul_log_pow_four_div_le : ξ² log⁴ ξ / L² ≤ (log log 3y)^{-2/5}.

The growth factor (1 + t² log⁵ t / L²)^{5(t-a)}

theorem IwaniecLinearSieve.hasDerivAt_lsx (L : ℝ) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (t : ℝ) => t ^ 2 * Real.log t ^ 5 / L ^ 2) ((2 * t * Real.log t ^ 5 + 5 * t * Real.log t ^ 4) / L ^ 2) t

theorem IwaniecLinearSieve.lsx_nonneg (L : ℝ) {t : ℝ} (ht : 1 ≤ t) : 0 ≤ t ^ 2 * Real.log t ^ 5 / L ^ 2

theorem IwaniecLinearSieve.hasDerivAt_growth (L a : ℝ) {t : ℝ} (ht : 1 ≤ t) : HasDerivAt (fun (t : ℝ) => (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2) ^ (5 * (t - a))) ((1 + t ^ 2 * Real.log t ^ 5 / L ^ 2) ^ (5 * (t - a)) * (5 * Real.log (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2) + 5 * (t - a) * ((2 * t * Real.log t ^ 5 + 5 * t * Real.log t ^ 4) / L ^ 2) / (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2))) t

theorem IwaniecLinearSieve.rate_bound_of_small_weight {u W E : ℝ} (hu : 32 ≤ u) (hW0 : 0 ≤ W) (hW : W ≤ 1 / 160) (hE : 4 * E ≤ W * (60 * u + 100)) : 4 * E ≤ u - 1 ∧ 4 * E * (1 + 5 * (W * u)) ≤ 5 * (W * u) * u

The scalar consequences of 4E ≤ W(60u + 100) when u ≥ 32 and 0 ≤ W ≤ 1/160.

theorem IwaniecLinearSieve.rate_bound {L a t : ℝ} (ha : 0 ≤ a) (ha1 : a ≤ 1) (ht1 : 1 ≤ t) (ht : 32 ≤ Real.log t) (hw : t ^ 2 * Real.log t ^ 4 / L ^ 2 ≤ 1 / 160) : 0 ≤ 5 * Real.log (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2) + 5 * (t - a) * ((2 * t * Real.log t ^ 5 + 5 * t * Real.log t ^ 4) / L ^ 2) / (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2) ∧ 4 * (5 * Real.log (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2) + 5 * (t - a) * ((2 * t * Real.log t ^ 5 + 5 * t * Real.log t ^ 4) / L ^ 2) / (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2)) ≤ Real.log t - 1 ∧ 4 * (5 * Real.log (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2) + 5 * (t - a) * ((2 * t * Real.log t ^ 5 + 5 * t * Real.log t ^ 4) / L ^ 2) / (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2)) * (1 + 5 * (t ^ 2 * Real.log t ^ 5 / L ^ 2)) ≤ 5 * (t ^ 2 * Real.log t ^ 5 / L ^ 2) * Real.log t

The logarithmic derivative of (1 + x)^{5(t-a)} is at most w (15 log t + 25); the consequences used below.

The Corollary to Lemma 10 in the form used here

theorem IwaniecLinearSieve.majG_succ_mul_log_lt (r : ℕ) {t : ℝ} (ht : 2 ≤ t) : majG (r + 1) t * Real.log t < 4 * (majG r (t - 1) * t / (t - 1) ^ 2)

theorem IwaniecLinearSieve.five_add_neg_one_pow_div_le (r : ℕ) : (5 + (-1) ^ r) / 2 ≤ 3

The range e^{32} ≤ t ≤ b, 160 b² log⁴ b ≤ L²

theorem IwaniecLinearSieve.range_facts {L t b : ℝ} (ht : Real.exp 32 ≤ t) (htb : t ≤ b) (hb : b ^ 2 * Real.log b ^ 4 ≤ L ^ 2 / 160) : 1 ≤ t ∧ 32 ≤ Real.log t ∧ t ^ 2 * Real.log t ^ 4 / L ^ 2 ≤ 1 / 160 ∧ 0 < L ^ 2

On [e^{32}, b] with 160 b² log⁴ b ≤ L²: 1 ≤ t, 32 ≤ log t and 160 w(t) ≤ 1.

theorem IwaniecLinearSieve.rpow_five_mul_sub_one {x : ℝ} (hx : 0 < x) (t : ℝ) : x ^ (5 * (t - 1)) = x ^ (5 * t) / x ^ 5

(1 + x)^{5(t-1)} = (1 + x)^{5t} / (1 + x)^5.

theorem IwaniecLinearSieve.continuousAt_growth (L a : ℝ) {t : ℝ} (ht : 1 ≤ t) : ContinuousAt (fun (t : ℝ) => (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2) ^ (5 * (t - a))) t

theorem IwaniecLinearSieve.continuousOn_lemma11_integrand (L : ℝ) (r : ℕ) {s b : ℝ} (hs : 2 ≤ s) : ContinuousOn (fun (t : ℝ) => (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2) ^ (5 * (t - 1)) * majG r (t - 1) * t / (t - 1) ^ 2) (Set.Icc s b)

theorem IwaniecLinearSieve.delta_eq_growth (s y : ℝ) : delta s y = (1 + s ^ 2 * Real.log s ^ 5 / Real.log y ^ 2) ^ (5 * (s - 0))

theorem IwaniecLinearSieve.delta_pos {s : ℝ} (hs : 1 ≤ s) (y : ℝ) : 0 < delta s y

theorem IwaniecLinearSieve.lemma11_decay_bound {x E G K ℓ : ℝ} (hx : 0 ≤ x) (hE : 0 ≤ E) (hK : 0 ≤ K) (hℓ : 0 < ℓ) (hG : G * ℓ ≤ 4 * K) (hrate : 4 * E * (1 + 5 * x) ≤ 5 * x * ℓ) : K / (1 + x) ^ 5 ≤ K - E * G

The algebraic decay estimate in Lemma 11: the bound on the growth rate E and G ℓ ≤ 4K imply K / (1 + x)⁵ ≤ K - EG.

theorem IwaniecLinearSieve.lemma11 (r : ℕ) {y s b : ℝ} (hs : Real.exp 32 ≤ s) (hsb : s ≤ b) (hb : b ^ 2 * Real.log b ^ 4 ≤ Real.log y ^ 2 / 160) : ∫ (t : ℝ) in s..b, (1 + t ^ 2 * Real.log t ^ 5 / Real.log y ^ 2) ^ (5 * (t - 1)) * majG r (t - 1) * t / (t - 1) ^ 2 < delta s y * majG (r + 1) s

[I71, Lemma 11] ((3.15)), with s₀ = e^{32}, c₃ = 4, and the upper limit ξ replaced by any b with 160 b² log⁴ b ≤ log² y: ∫_s^b (1 + t² log⁵ t / L²)^{5(t-1)} G_r(t-1) t/(t-1)² dt < δ(s, y) G_{r+1}(s).

Lemma 12 and the monotonicity used in Corollary 3

theorem IwaniecLinearSieve.four_lt_of_exp_le {t : ℝ} (ht : Real.exp 32 ≤ t) : 4 < t

theorem IwaniecLinearSieve.growth_le_decay {E G K ℓ : ℝ} (hG : 0 ≤ G) (hE : 4 * E ≤ ℓ) (hdecay : G * ℓ ≤ 4 * K) : E * G ≤ K

If the growth rate satisfies 4E ≤ ℓ and the decay satisfies Gℓ ≤ 4K, then EG ≤ K for G ≥ 0. This is the scalar comparison used in Lemma 12.

theorem IwaniecLinearSieve.antitoneOn_growth_mul {L s b : ℝ} {g k ℓ : ℝ → ℝ} (hs : Real.exp 32 ≤ s) (hb : b ^ 2 * Real.log b ^ 4 ≤ L ^ 2 / 160) (hg : ∀ t ∈ Set.Icc s b, HasDerivAt g (-k t) t) (hg0 : ∀ t ∈ Set.Icc s b, 0 ≤ g t) (hgk : ∀ t ∈ Set.Icc s b, g t * ℓ t ≤ 4 * k t) (hℓ : ∀ t ∈ Set.Icc s b, Real.log t - 1 ≤ ℓ t) : AntitoneOn (fun (t : ℝ) => (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2) ^ (5 * (t - 1)) * g t) (Set.Icc s b)

If g ≥ 0 has derivative -k with g ℓ ≤ 4 k and ℓ ≥ log t - 1, then (1 + x)^{5(t-1)} g(t) is antitone on [s, b] (for e^{32} ≤ s, 160 b² log⁴ b ≤ L²).

theorem IwaniecLinearSieve.lemma12 (r : ℕ) {L s b : ℝ} (hs : Real.exp 32 ≤ s) (hb : b ^ 2 * Real.log b ^ 4 ≤ L ^ 2 / 160) : AntitoneOn (fun (t : ℝ) => (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2) ^ (5 * (t - 1)) * majG (r + 1) t) (Set.Icc s b)

[I71, Lemma 12]: μ(t) = (1 + t² log⁵ t / L²)^{5(t-1)} G_{r+1}(t) is antitone on [s, b] for e^{32} ≤ s and 160 b² log⁴ b ≤ L².

theorem IwaniecLinearSieve.log_sub_one_ge {t : ℝ} (ht : 2 ≤ t) : Real.log t - 1 ≤ Real.log (t - 1)

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

theorem IwaniecLinearSieve.antitoneOn_mul_of_nonneg {f g : ℝ → ℝ} {S : Set ℝ} (hf : AntitoneOn f S) (hg : AntitoneOn g S) (hf0 : ∀ t ∈ S, 0 ≤ f t) (hg0 : ∀ t ∈ S, 0 ≤ g t) : AntitoneOn (fun (t : ℝ) => f t * g t) S

theorem IwaniecLinearSieve.antitoneOn_cor3Weight (r : ℕ) {L s b : ℝ} (hs : Real.exp 32 ≤ s) (hb : b ^ 2 * Real.log b ^ 4 ≤ L ^ 2 / 160) : AntitoneOn (fun (t : ℝ) => (1 + t ^ 2 * Real.log t ^ 5 / L ^ 2) ^ (5 * (t - 1)) * majG r (t - 1) * (t ^ 2 / (t - 1) ^ 2)) (Set.Icc s b)

The weight in the proof of [I71, Corollary 3]: (1 + t² log⁵ t / L²)^{5(t-1)} G_r(t-1) t²/(t-1)² is antitone on [s, b].

The size of ξ

theorem IwaniecLinearSieve.xi_sq_mul_log_pow_four_div_le {y : ℝ} (hy : 1 < y) (hℓ : 1 ≤ Real.log (Real.log (3 * y))) (hξ : 1 ≤ xi y) : xi y ^ 2 * Real.log (xi y) ^ 4 / Real.log y ^ 2 ≤ Real.log (Real.log (3 * y)) ^ (-(2 / 5))

ξ² log⁴ ξ / L² ≤ (log log 3y)^{-2/5} (cf. [I71, proof of Lemma 11]).

theorem IwaniecLinearSieve.tendsto_log_log_three_mul : Filter.Tendsto (fun (y : ℝ) => Real.log (Real.log (3 * y))) Filter.atTop Filter.atTop

theorem IwaniecLinearSieve.tendsto_xi : Filter.Tendsto xi Filter.atTop Filter.atTop

ξ(y) → ∞.

theorem IwaniecLinearSieve.exists_xi_large : ∃ (y₀ : ℝ), ∀ y ≥ y₀, 1 < y ∧ Real.exp 32 ≤ xi y ∧ xi y ^ 2 * Real.log (xi y) ^ 4 ≤ Real.log y ^ 2 / 160 ∧ 2 ≤ y ^ (1 / xi y)

For y large: ξ(y) ≥ e^{32}, 160 ξ² log⁴ ξ ≤ log² y and y^{1/ξ} ≥ 2, so that Lemmas 11, 12 and Corollary 3 apply up to b = ξ(y).