The linear sieve at level C₀ z² ([I71, Theorems 4–5]; [I78, Lemma 2])

With y = C₀ z² the sifting parameter is s = log y / log z = 2 + log C₀ / log z. Theorem 4, f(s) ≤ s - 3 log(s - 1) (from f(2) = 2) and R_asymp show that the deficit R(z) - V⁻(y, z) of the lower-bound sieve is at most R(z) (1 - 1/log z) once log C₀ exceeds the error constant of Theorem 4, so the main term is ≥ R(z)/log z; Theorem 5 bounds the support by ≪ z²/log² z.

def IwaniecLinearSieve.LinearSieveEstimate : Prop

The estimates for Rosser's lower-bound sieve at level y = C₀ z² which [I78, Lemma 2] quotes from [I71]: with s = log y / log z = 2 + log C₀ / log z,

• (6) ∑_{n ∣ P} σ_n / φ(n) = (∑_{d ∈ D⁻} μ(d)/d) / R(z) ≥ c / log z, i.e. R(z) - ∑_{d ∈ D⁻} μ(d)/d ≤ R(z) (1 - c / log z);
• (5) ∑ |λ_n| = |D⁻| ≪ y / log² y ≪ z² / log² z,

for all z ≥ z₀.

Equations

• One or more equations did not get rendered due to their size.

theorem IwaniecLinearSieve.rpow_one_div_log_div {y z : ℝ} (hy : 0 < y) (hz : 1 < z) (hyl : Real.log y ≠ 0) : y ^ (1 / (Real.log y / Real.log z)) = z

y^{1/s} = z for y = C₀ z² and s = log y / log z.

theorem IwaniecLinearSieve.div_one_add_le_log_one_add {x : ℝ} (hx : 0 ≤ x) : x / (1 + x) ≤ Real.log (1 + x)

log (1 + x) ≥ x / (1 + x) for x ≥ 0.

theorem IwaniecLinearSieve.two_mul_div_three_le_log_sub_one {x s : ℝ} (hx : 0 ≤ x) (hxhalf : x ≤ 1 / 2) (hs : 2 + x ≤ s) : 2 * x / 3 ≤ Real.log (s - 1)

If 0 ≤ x ≤ 1/2 and s ≥ 2 + x, then log(s - 1) ≥ 2x/3. This supplies the logarithmic gain in the linear sieve estimate and Theorem 2.

theorem IwaniecLinearSieve.tendsto_pntE_mul_log : Filter.Tendsto (fun (z : ℝ) => pntE z * Real.log z) Filter.atTop (nhds 0)

pntE z · log z → 0.

theorem IwaniecLinearSieve.sieve_error_absorption {A B s ℓ : ℝ} (hA : A = B + 5) (hB : 0 ≤ B) (hs2 : 2 ≤ s) (hs25 : s ≤ 5 / 2) (hℓ : 0 < ℓ) : (s - 2 * A / ℓ) / (s * ℓ) + B / (s * ℓ) ^ 2 ≤ 1 / ℓ - 4 / ℓ ^ 2

For 2 ≤ s ≤ 5/2, choosing A = B + 5 absorbs the bounded sieve error B and leaves a saving of 4/ℓ².

theorem IwaniecLinearSieve.pnt_error_absorption {c e ℓ : ℝ} (hℓ : 0 < ℓ) (he0 : 0 ≤ e) (he : e * ℓ ≤ 3 * c) : c / ℓ - 4 * c / ℓ ^ 2 ≤ (c - e) / ℓ * (1 - 1 / ℓ)

If the PNT error e satisfies eℓ ≤ 3c, the saving 4c/ℓ² leaves the factor 1 - 1/ℓ against the lower estimate (c - e)/ℓ for R(z).

theorem IwaniecLinearSieve.linearSieveEstimate : LinearSieveEstimate

[I78, Lemma 2], from [I71, Theorems 4 and 5]: at level C₀ z² the Rosser lower-bound sieve leaves a main term ≫ R(z)/log z, and its support has size ≪ z² / log² z.