[I71, Lemmas 8, 9 (lower bound), 10]

• Lemma 8: 𝔐(s-1) < 4 s² 𝔐(s) for s ≥ 3.
• Lemma 10: log t 𝔐(t) < 2 t/(t-1)² 𝔐(t-1) for t ≥ 2; hence 𝔐(t) t log t / 𝔐(t-1) < 9/2 for t ≥ 3, and the Corollary G_{r+1}(t) (t-1)² log t / (G_r(t-1) t) < 4 for t ≥ 2.
• Lemma 9 (lower bound): G_r(s) ≥ exp(-s log s - s log log s - c s) for s ≥ 3.

[I71] proves Lemma 10 assuming that 𝔐(t-1)/𝔐(t) is increasing; we instead use a first crossing argument for the inequality itself (cf. [Opera de Cribro, Lemma 11.7]). For Lemma 9 we compare 𝔐 with the explicit subsolution exp(-(s log s + s log log s + 2s)) of (3.12), instead of quoting the asymptotics of Hua's book.

Lemma 8

theorem IwaniecLinearSieve.bigM_sub_half_le {s : ℝ} (hs : 3 ≤ s) : bigM (s - 1 / 2) ≤ 2 * (s - 1) ^ 2 / s * bigM s

From (3.12): 𝔐(s - 1/2) ≤ 2(s-1)²/s 𝔐(s) for s ≥ 3.

theorem IwaniecLinearSieve.bigM_sub_one_lt {s : ℝ} (hs : 3 ≤ s) : bigM (s - 1) < 4 * s ^ 2 * bigM s

[I71, Lemma 8]: 𝔐(s-1) < 4 s² 𝔐(s) for s ≥ 3.

theorem IwaniecLinearSieve.bigM_sub_one_div_lt {s : ℝ} (hs : 3 ≤ s) : bigM (s - 1) / bigM s < 4 * s ^ 2

[I71, Lemma 8] in ratio form.

Lemma 10

theorem IwaniecLinearSieve.integral_exp_neg_mul_unit (a : ℝ) {l : ℝ} (hl : l ≠ 0) : ∫ (x : ℝ) in a..a + 1, Real.exp (-(l * (x - a))) = (1 - Real.exp (-l)) / l

∫_{a}^{a+1} exp(-λ(x - a)) dx = (1 - exp(-λ))/λ.

theorem IwaniecLinearSieve.log_four_lt : Real.log 4 < 1.3863

theorem IwaniecLinearSieve.log_mul_ratio_lt {t q L : ℝ} (ht0 : 0 < t) (hq1 : 1 < q) (hq2 : q ^ 2 = t - 1) (hL : 1 < L) (hLt : Real.log t ≤ L + 1 / (t - 1)) : Real.log t * (t / ((t - 1) ^ 2 - 1 / 2) * ((1 - q⁻¹) / (L / 2))) < 2 * (t / (t - 1) ^ 2)

The numerical comparison in the main range of Lemma 10. With q² = t - 1, the logarithmic bound makes the integrated exponential estimate smaller than 2t/(t-1)².

theorem IwaniecLinearSieve.log_mul_bigM_lt {t : ℝ} (ht : 2 ≤ t) : Real.log t * bigM t < 2 * (t / (t - 1) ^ 2) * bigM (t - 1)

The inequality behind [I71, Lemma 10]: log t · 𝔐(t) < 2 t/(t-1)² · 𝔐(t-1) for t ≥ 2.

theorem IwaniecLinearSieve.bigM_mul_log_div_lt {t : ℝ} (ht : 3 ≤ t) : bigM t * t * Real.log t / bigM (t - 1) < 9 / 2

[I71, Lemma 10]: 𝔐(t) t log t / 𝔐(t-1) < 9/2 for t ≥ 3 (so it is O(1)).

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

Corollary to [I71, Lemma 10]: G_{r+1}(t) (t-1)² log t / (G_r(t-1) t) < 4 for t ≥ 2 (and all r; [I71] states it for t > (5 + (-1)^r)/2).

Lemma 9 (lower bound)

noncomputable def IwaniecLinearSieve.lemma9Fun (s : ℝ) : ℝ

The comparison function exp(-(s log s + s log log s + 2 s)) for [I71, Lemma 9].

Equations

• IwaniecLinearSieve.lemma9Fun s = Real.exp (-(s * Real.log s + s * Real.log (Real.log s) + 2 * s))

theorem IwaniecLinearSieve.continuousOn_lemma9Fun : ContinuousOn lemma9Fun (Set.Ici 3)

theorem IwaniecLinearSieve.one_le_log_of_three_le {x : ℝ} (hx : 3 ≤ x) : 1 ≤ Real.log x

theorem IwaniecLinearSieve.lemma9Fun_le_one {x : ℝ} (hx : 3 ≤ x) : lemma9Fun x ≤ 1

theorem IwaniecLinearSieve.lemma9_phi_sub {s x : ℝ} (hs : 4 ≤ s) (hx : s - 1 ≤ x) (hxs : x ≤ s) : (Real.log (s - 1) + Real.log (Real.log (s - 1)) + 3) * (s - x) ≤ s * Real.log s + s * Real.log (Real.log s) + 2 * s - (x * Real.log x + x * Real.log (Real.log x) + 2 * x)

Convexity estimate: φ(s) - φ(x) ≥ λ (s - x) for 3 ≤ s - 1 ≤ x ≤ s, where φ(s) = s log s + s log log s + 2s and λ = log(s-1) + log log(s-1) + 3.

theorem IwaniecLinearSieve.lemma9Fun_weighted_exp_le {s x : ℝ} (hs : 4 ≤ s) (hx : s - 1 ≤ x) (hxs : x ≤ s) : have l := Real.log (s - 1) + Real.log (Real.log (s - 1)) + 3; (1 - 1 / (2 * (s - 1) ^ 2)) * (lemma9Fun s * Real.exp l) * Real.exp (-(l * (x - (s - 1)))) ≤ (1 - 1 / (2 * x ^ 2)) * lemma9Fun x

On [s-1, s], convexity of the exponent gives an exponential lower bound for the weighted comparison function in (3.12).

theorem IwaniecLinearSieve.lemma9_integral_factor_ge_one {s : ℝ} (hs : 4 ≤ s) : have l := Real.log (s - 1) + Real.log (Real.log (s - 1)) + 3; 1 ≤ (1 - 1 / (2 * (s - 1) ^ 2)) * (Real.exp l * ((1 - Real.exp (-l)) / l)) * (s / ((s - 1) ^ 2 - 1 / 2))

The exponential lower bound, integrated and multiplied by the factor in (3.12), has coefficient at least one. The key estimate is l (s-1)² ≤ s (exp l - 1).

theorem IwaniecLinearSieve.lemma9Fun_le_integral {s : ℝ} (hs : 4 ≤ s) : lemma9Fun s ≤ s / ((s - 1) ^ 2 - 1 / 2) * ∫ (x : ℝ) in s - 1..s, (1 - 1 / (2 * x ^ 2)) * lemma9Fun x

lemma9Fun is a subsolution of (3.12) for s ≥ 4.

theorem IwaniecLinearSieve.bigM_gt_lemma9Fun {s : ℝ} (hs : 3 ≤ s) : bigM 4 / 2 * lemma9Fun s < bigM s

Comparison of 𝔐 with the subsolution lemma9Fun: 𝔐(s) > (𝔐(4)/2) lemma9Fun(s) for s ≥ 3.

theorem IwaniecLinearSieve.bigM_ge_exp : ∃ κ > 0, ∀ s ≥ 3, κ * Real.exp (-(s * Real.log s + s * Real.log (Real.log s) + 2 * s)) ≤ bigM s

[I71, Lemma 9], lower bound for 𝔐: there is κ > 0 with 𝔐(s) ≥ κ exp(-(s log s + s log log s + 2 s)) for s ≥ 3.

theorem IwaniecLinearSieve.majG_ge_exp : ∃ (c : ℝ), ∀ (r : ℕ) (s : ℝ), 3 ≤ s → Real.exp (-(s * Real.log s) - s * Real.log (Real.log s) - c * s) ≤ majG r s

[I71, Lemma 9], lower bound: there is c with G_r(s) ≥ exp(-s log s - s log log s - c s) for all r and s ≥ 3.