Real-analysis facts for large y in [I71, Theorem 4]

With L = log y, ℓ = log log 3y, Λ = log log y, ξ = ξ(y) = L / ℓ^{11/5} and w = y^{1/ξ} (so log w = ℓ^{11/5} and pntE w = exp (-κ ℓ^{11/10})):

• eventually_delta_mul_le: δ(s₀, y) (1 + C ξ² pntE w) ≤ 1 + Λ² / (8 L²) ([I71, (4.6)]);
• eventually_mul_pntE_le: K ξ² L³ pntE w ≤ 1 ([I71, (4.2), (4.3)]);
• eventually_crude: the crude bound 2 (e X/(ξ-2))^{ξ-2} for the depth sums at w (with X = log log w + C') times L⁴ is below the Lemma 9 lower bound for G(ξ/2) and below δ(ξ/2, y) times the Lemma 9 lower bound for G(ξ) ([I71, (4.4), (4.5), (4.9), (4.10)]).

L, ξ, w in terms of ℓ = log log 3y

theorem IwaniecLinearSieve.TheoremFour.loglog_three_mul_pos {y : ℝ} (hy : 1 < y) : 0 < Real.log (Real.log (3 * y))

theorem IwaniecLinearSieve.TheoremFour.log_add_log_three {y : ℝ} (hy : 1 < y) : Real.log y + Real.log 3 = Real.exp (Real.log (Real.log (3 * y)))

theorem IwaniecLinearSieve.TheoremFour.xi_mul_rpow {y : ℝ} (hy : 1 < y) : xi y * Real.log (Real.log (3 * y)) ^ (11 / 5) = Real.log y

theorem IwaniecLinearSieve.TheoremFour.pntE_rpow_one_div_xi {y : ℝ} (hy : 1 < y) : pntE (y ^ (1 / xi y)) = Real.exp (-pntκ * Real.log (Real.log (3 * y)) ^ (11 / 10))

theorem IwaniecLinearSieve.TheoremFour.xi_nonneg {y : ℝ} (hy : 1 < y) : 0 ≤ xi y

theorem IwaniecLinearSieve.TheoremFour.xi_le_log {y : ℝ} (hy : 1 < y) (hℓ : 1 ≤ Real.log (Real.log (3 * y))) : xi y ≤ Real.log y

L⁵ pntE(w) → 0

theorem IwaniecLinearSieve.TheoremFour.tendsto_lin_sub_rpow : Filter.Tendsto (fun (ℓ : ℝ) => 5 * ℓ - pntκ * ℓ ^ (11 / 10)) Filter.atTop Filter.atBot

theorem IwaniecLinearSieve.TheoremFour.tendsto_log_pow_pntE : Filter.Tendsto (fun (y : ℝ) => Real.log y ^ 5 * pntE (y ^ (1 / xi y))) Filter.atTop (nhds 0)

theorem IwaniecLinearSieve.TheoremFour.eventually_one_le_loglog : ∀ᶠ (y : ℝ) in Filter.atTop, 1 ≤ Real.log (Real.log y)

theorem IwaniecLinearSieve.TheoremFour.eventually_mul_pntE_le (K : ℝ) : ∀ᶠ (y : ℝ) in Filter.atTop, K * xi y ^ 2 * Real.log y ^ 3 * pntE (y ^ (1 / xi y)) ≤ 1

theorem IwaniecLinearSieve.TheoremFour.exp_le_one_add_two_mul {v : ℝ} (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : Real.exp v ≤ 1 + 2 * v

On [0, 1], the exponential is at most 1 + 2v.

theorem IwaniecLinearSieve.TheoremFour.eventually_delta_mul_le (C : ℝ) (hC : 0 ≤ C) : ∀ᶠ (y : ℝ) in Filter.atTop, delta (Real.exp 32) y * (1 + C * xi y ^ 2 * pntE (y ^ (1 / xi y))) ≤ 1 + Real.log (Real.log y) ^ 2 / (8 * Real.log y ^ 2)

The crude bound against the Lemma 9 lower bounds

theorem IwaniecLinearSieve.TheoremFour.mul_log_sub_le {ξ : ℝ} (hξ : 2 < ξ) : ξ * Real.log ξ - (ξ - 2) * Real.log (ξ - 2) ≤ 2 * Real.log ξ + 2

ξ log ξ - (ξ - 2) log (ξ - 2) ≤ 2 log ξ + 2.

theorem IwaniecLinearSieve.TheoremFour.crude_half_exponent_le {c ℓ L ξ X : ℝ} (hℓ_large : 2 ≤ ℓ) (hxi_large : 8 * ℓ ≤ ξ) (hlogL_upper : Real.log L ≤ ℓ) (hlogX_nonneg : 0 ≤ Real.log X) (hlogX_upper : Real.log X ≤ Real.log ℓ / 4) (hlog_shift_lower : Real.log (ξ / 2) ≤ Real.log (ξ - 2)) (hlog_half_lower : ℓ / 2 ≤ Real.log (ξ / 2)) (hloglog_half_upper : Real.log (Real.log (ξ / 2)) ≤ Real.log ℓ) (herror_budget : 2 + c / 2 + 3 / 4 * Real.log ℓ ≤ ℓ / 8) : Real.log 2 + (-((ξ - 2) * Real.log (ξ - 2)) + (ξ - 2) * Real.log X + (ξ - 2)) + 4 * Real.log L ≤ -(ξ / 2 * Real.log (ξ / 2)) - ξ / 2 * Real.log (Real.log (ξ / 2)) - c * (ξ / 2)

The exponent comparison for [I71, (4.4), (4.9)], after bounding the logarithms.

theorem IwaniecLinearSieve.TheoremFour.crude_full_exponent_le {c ℓ L ξ X x : ℝ} (hℓ_large : 2 ≤ ℓ) (hxi_large : 8 * ℓ ≤ ξ) (hlogL_upper : Real.log L ≤ ℓ) (hlogX_nonneg : 0 ≤ Real.log X) (hlogX_upper : Real.log X ≤ Real.log ℓ / 4) (hlogxi_upper : Real.log ξ ≤ ℓ) (hloglogxi_upper : Real.log (Real.log ξ) ≤ Real.log ℓ) (hlogx_lower : 3 / 5 * Real.log ℓ - 7 * Real.log 2 ≤ Real.log x) (herror_budget : 2 + c + 18 * Real.log 2 ≤ Real.log ℓ / 4) : Real.log 2 + (-((ξ - 2) * Real.log (ξ - 2)) + (ξ - 2) * Real.log X + (ξ - 2)) + 4 * Real.log L ≤ Real.log x * (5 * (ξ / 2)) + (-(ξ * Real.log ξ) - ξ * Real.log (Real.log ξ) - c * ξ)

The exponent comparison for [I71, (4.5), (4.10)], using the lower bound on log x.

theorem IwaniecLinearSieve.TheoremFour.crude_alg {c C' ℓ L ξ : ℝ} (hC' : 1 ≤ C') (hℓ : 2 ≤ ℓ) (hL : L + Real.log 3 = Real.exp ℓ) (hξ : ξ * ℓ ^ (11 / 5) = L) (h2 : 2 * Real.log 3 ≤ Real.exp ℓ) (h3 : 4 * ℓ ^ (11 / 5) ≤ Real.exp (ℓ / 2)) (h4 : 11 / 5 * Real.log ℓ + C' ≤ ℓ ^ (1 / 4)) (h5 : 2 + c + 18 * Real.log 2 ≤ Real.log ℓ / 4) (h6 : 2 + c / 2 + 3 / 4 * Real.log ℓ ≤ ℓ / 8) : 0 < 11 / 5 * Real.log ℓ + C' ∧ 2 * Real.exp 1 * (11 / 5 * Real.log ℓ + C') ≤ ξ - 2 ∧ 2 * (Real.exp 1 * (11 / 5 * Real.log ℓ + C') / (ξ - 2)) ^ (ξ - 2) * L ^ 4 ≤ Real.exp (-(ξ / 2 * Real.log (ξ / 2)) - ξ / 2 * Real.log (Real.log (ξ / 2)) - c * (ξ / 2)) ∧ 2 * (Real.exp 1 * (11 / 5 * Real.log ℓ + C') / (ξ - 2)) ^ (ξ - 2) * L ^ 4 ≤ (1 + (ξ / 2) ^ 2 * Real.log (ξ / 2) ^ 5 / L ^ 2) ^ (5 * (ξ / 2)) * Real.exp (-(ξ * Real.log ξ) - ξ * Real.log (Real.log ξ) - c * ξ)

The comparisons [I71, (4.4), (4.5), (4.9), (4.10)] in the variable ℓ = log log 3y, with L = e^ℓ - log 3 and ξ = L / ℓ^{11/5}, under explicit "ℓ large" hypotheses.

theorem IwaniecLinearSieve.TheoremFour.eventually_crude_hyp (c C' : ℝ) : ∀ᶠ (ℓ : ℝ) in Filter.atTop, 2 ≤ ℓ ∧ 2 * Real.log 3 ≤ Real.exp ℓ ∧ 4 * ℓ ^ (11 / 5) ≤ Real.exp (ℓ / 2) ∧ 11 / 5 * Real.log ℓ + C' ≤ ℓ ^ (1 / 4) ∧ 2 + c + 18 * Real.log 2 ≤ Real.log ℓ / 4 ∧ 2 + c / 2 + 3 / 4 * Real.log ℓ ≤ ℓ / 8

The "ℓ large" hypotheses of crude_alg hold eventually.

theorem IwaniecLinearSieve.TheoremFour.eventually_crude (c C' : ℝ) (hC' : 1 ≤ C') : ∀ᶠ (y : ℝ) in Filter.atTop, 0 < Real.log (Real.log (y ^ (1 / xi y))) + C' ∧ 2 * Real.exp 1 * (Real.log (Real.log (y ^ (1 / xi y))) + C') ≤ xi y - 2 ∧ 2 * (Real.exp 1 * (Real.log (Real.log (y ^ (1 / xi y))) + C') / (xi y - 2)) ^ (xi y - 2) * Real.log y ^ 4 ≤ Real.exp (-(xi y / 2 * Real.log (xi y / 2)) - xi y / 2 * Real.log (Real.log (xi y / 2)) - c * (xi y / 2)) ∧ 2 * (Real.exp 1 * (Real.log (Real.log (y ^ (1 / xi y))) + C') / (xi y - 2)) ^ (xi y - 2) * Real.log y ^ 4 ≤ delta (xi y / 2) y * Real.exp (-(xi y * Real.log (xi y)) - xi y * Real.log (Real.log (xi y)) - c * xi y)