Real-variable estimates for [I71, Theorem 5]

With L = log y, λ = log log 3y (TheoremFive.lam) and ξ = L / λ^{11/5} (xi), this file collects the "for y ≥ y₀" facts used in the proof of Theorem 5:

• eventually_scalar: λ, log λ, λ^{1/5} are large, λ - 1 ≤ log L ≤ λ, 24 λ ≤ ξ, 16 λ² ≤ L, λ/2 ≤ log (ξ/2), 4 log λ + c ≤ log ξ ≤ λ;
• crude_exponent_le: the comparison of the crude count of rosserSet lower y y^{1/(ξ-1)} with y exp(-ξ log ξ + (3/2) ξ log λ) / (8 L⁴) ([I71, p. 27]);
• exists_slack: the losses δ(e^{32}, y) (1 + C ξ² pntE(y^{1/ξ})) - 1 of Corollary 3 are at most (log log y)² / (8 L²), reusing TheoremFour.eventually_delta_mul_le.

noncomputable def IwaniecLinearSieve.TheoremFive.lam (y : ℝ) : ℝ

λ(y) = log log 3y, the denominator variable of ξ(y) = log y / λ^{11/5}.

Equations

• IwaniecLinearSieve.TheoremFive.lam y = Real.log (Real.log (3 * y))

theorem IwaniecLinearSieve.TheoremFive.xi_eq_lam (y : ℝ) : xi y = Real.log y / lam y ^ (11 / 5)

theorem IwaniecLinearSieve.TheoremFive.tendsto_lam : Filter.Tendsto lam Filter.atTop Filter.atTop

theorem IwaniecLinearSieve.TheoremFive.eventually_add_mul_log_le (α β : ℝ) : ∀ᶠ (x : ℝ) in Filter.atTop, α + β * Real.log x ≤ x

α + β log x ≤ x for large x.

theorem IwaniecLinearSieve.TheoremFive.one_lt_log_three : 1 < Real.log 3

theorem IwaniecLinearSieve.TheoremFive.lam_pos {y : ℝ} (hy : 1 < y) : 0 < lam y

theorem IwaniecLinearSieve.TheoremFive.log_xi_eq {y : ℝ} (hy : 1 < y) : Real.log (xi y) = Real.log (Real.log y) - 11 / 5 * Real.log (lam y)

log ξ = log L - (11/5) log λ.

theorem IwaniecLinearSieve.TheoremFive.xi_pos {y : ℝ} (hy : 1 < y) : 0 < xi y

theorem IwaniecLinearSieve.TheoremFive.eventually_scalar (c : ℝ) (hc : 100 ≤ c) : ∀ᶠ (y : ℝ) in Filter.atTop, 3 ≤ y ∧ c ≤ Real.log (lam y) ∧ c ≤ lam y ^ (1 / 5) ∧ c ≤ lam y ∧ Real.log (Real.log y) ≤ lam y ∧ lam y - 1 ≤ Real.log (Real.log y) ∧ 24 * lam y ≤ xi y ∧ 16 * lam y ^ 2 ≤ Real.log y ∧ lam y / 2 ≤ Real.log (xi y / 2) ∧ 4 * Real.log (lam y) + c ≤ Real.log (xi y) ∧ Real.log (xi y) ≤ lam y

The scalar facts about L = log y, λ = lam y and ξ = xi y used for Theorem 5, valid for large y; c ≥ 100 is a free threshold.

The crude part ([I71, p. 27])

theorem IwaniecLinearSieve.TheoremFive.crude_exponent_le {L ℓ lam ξ a : ℝ} (hL : 0 < L) (hℓ : ℓ = Real.log L) (hℓlam : ℓ ≤ lam) (hlam : 100 ≤ lam) (ha : 12 ≤ a) (hxilam : 4 * (ξ * lam ^ 2) ≤ L) (h24 : 24 * lam ≤ ξ) (h16 : 16 * lam ^ 2 ≤ L) (hlogξ : Real.log ξ ≤ lam) : 8 * L ^ 4 * (1 + Real.exp (L + 2 * ξ - L / lam) + 2 * Real.exp (L - ξ * Real.log ξ + ξ * a + 5 * ξ)) ≤ Real.exp (L - ξ * Real.log ξ + 3 / 2 * ξ * a)

The comparison at the bottom of [I71, p. 27], in exponential form: with ℓ = log L, 8 L⁴ (1 + e^{L + 2ξ - L/λ} + 2 e^{L - ξ log ξ + ξ a + 5ξ}) ≤ e^{L - ξ log ξ + (3/2) ξ a} (here a = log λ), under the scalar facts of eventually_scalar.

The slack ([I71, (4.2), (4.6)])

theorem IwaniecLinearSieve.TheoremFive.one_add_rpow_le_exp {x p : ℝ} (hx : 0 ≤ x) (hp : 0 ≤ p) : (1 + x) ^ p ≤ Real.exp (p * x)

(1 + x)^p ≤ e^{p x} for x ≥ 0, p ≥ 0.

theorem IwaniecLinearSieve.TheoremFive.exists_slack (C : ℝ) (hC : 0 ≤ C) : ∃ (y₀ : ℝ), ∀ y ≥ y₀, 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) ∧ 1 ≤ Real.log (Real.log y)

For every C ≥ 0 and large y, with s₀ = e^{32} and ℓ = log log y: δ(s₀, y) (1 + C ξ² pntE(y^{1/ξ})) - 1 ≤ ℓ² / (8 L²) and ℓ ≥ 1.