[I71, Theorem 4]

With L = log y, z = y^{1/s}, ξ = ξ(y), cR the constant of R_asymp, there is c₇ with fail lower r y z ≤ cR (M(s)/L + c₇ r/(r+1) δ(s, y) G(s)/L²)

for all r, y > 1, sMin lower ≤ s ≤ ξ(y).

The proof is by induction on r (for both sieves at once), as in [I71, pp. 23–25]:

• small y (y < y₀): the crude bound fail ≤ exp (SLT y₀) ([I71, (4.8)]);
• r + 2 > 2 L / log L: the recursion has stabilised, fail (r+1) = fail r;
• otherwise split the prime sum at w = y^{1/ξ} (fail_succ_le_split). For p ≥ w the inner level (y/p, t_p - 1) is in range (inner_le_xi), and the induction hypothesis, Corollary 1 and Corollary 3 give the main term and r/(r+1) times the error term; the primes p < w are fail (r+1) y w, bounded crudely. The losses are absorbed by (r+1)/(r+2) - r/(r+1) ≥ (r+1)/(r+2) · (log L)²/(4L²), as in [I71, (4.6)].

Compared with [I71] we split at y^{1/ξ} instead of y^{1/(ξ-1)} (then t_p - 1 ≤ ξ(y/p) holds exactly), use SLT(w) ≤ log log w + C in the crude bound, and the upper-sieve source term ∑_{y^{1/3} ≤ p < z} R(p)/p = R(y^{1/3}) - R(z) replaces [I71, Lemmas 14, 16].

def IwaniecLinearSieve.TheoremFour.Bound (cR c₇ : ℝ) (r : ℕ) : Prop

Theorem 4 at depth r with constants cR, c₇.

Equations

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

theorem IwaniecLinearSieve.TheoremFour.one_le_sMin (lower : Bool) : 1 ≤ sMin lower

The large primes: induction hypothesis, Corollaries 1 and 3

theorem IwaniecLinearSieve.TheoremFour.ih_term {cR c₇ : ℝ} {r : ℕ} (IH : Bound cR c₇ r) {lower : Bool} {y s : ℝ} {p : ℕ} (hy : 1 < y) (hs : sMin lower ≤ s) (hp : p ∈ rosserPrimes lower y (y ^ (1 / s))) (hw : y ^ (1 / xi y) ≤ ↑p) : fail (!lower) r (y / ↑p) ↑p / ↑p ≤ cR * (mainMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p))) + cR * c₇ * (↑r / (↑r + 1)) * (delta (Real.log y / Real.log ↑p - 1) (y / ↑p) * errMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p) ^ 2))

The induction hypothesis at the inner level (y/p, t_p - 1), divided by p.

theorem IwaniecLinearSieve.TheoremFour.sum_ih_le {cR c₇ : ℝ} {r : ℕ} (IH : Bound cR c₇ r) {lower : Bool} {y s : ℝ} (hy : 1 < y) (hs : sMin lower ≤ s) : ∑ p ∈ rosserPrimes lower y (y ^ (1 / s)) with y ^ (1 / xi y) ≤ ↑p, fail (!lower) r (y / ↑p) ↑p / ↑p ≤ cR * ∑ p ∈ rosserPrimes lower y (y ^ (1 / s)) with y ^ (1 / xi y) ≤ ↑p, mainMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p)) + cR * c₇ * (↑r / (↑r + 1)) * ∑ p ∈ rosserPrimes lower y (y ^ (1 / s)) with y ^ (1 / xi y) ≤ ↑p, delta (Real.log y / Real.log ↑p - 1) (y / ↑p) * errMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p) ^ 2)

theorem IwaniecLinearSieve.TheoremFour.intervalIntegral_le_integral_Ioi {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hf : MeasureTheory.IntegrableOn f (Set.Ioi a) MeasureTheory.volume) (hf0 : ∀ t ∈ Set.Ioi a, 0 ≤ f t) : ∫ (t : ℝ) in a..b, f t ≤ ∫ (t : ℝ) in Set.Ioi a, f t

theorem IwaniecLinearSieve.TheoremFour.cor1_part : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (lower : Bool) (y s : ℝ), 1 < y → sMin lower ≤ s → s ≤ xi y → 3 ≤ xi y → 2 ≤ y ^ (1 / xi y) → ∑ p ∈ rosserPrimes lower y (y ^ (1 / s)) with y ^ (1 / xi y) ≤ ↑p, mainMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p)) ≤ (mainMaj lower s - if lower = true then 0 else max (3 - s) 0) / Real.log y + C * s ^ 2 * errMaj lower s * pntE (y ^ (1 / xi y)) / Real.log y

Corollary 1 for the large primes: the main terms of the inner levels add up to M(s)/L (minus the source part (3 - s)⁺/L of the upper sieve), up to O(s² G(s) pntE(w)/L).

theorem IwaniecLinearSieve.TheoremFour.src_le_of_le_xi {cR CR : ℝ} (hR : ∀ z ≥ 2, |R z * Real.log z - cR| ≤ CR * pntE z) {lower : Bool} {y s : ℝ} (hy : 1 < y) (hs : sMin lower ≤ s) (hsξ : s ≤ xi y) (hξ3 : 3 ≤ xi y) (hw2 : 2 ≤ y ^ (1 / xi y)) : src lower y (y ^ (1 / s)) ≤ (if lower = true then 0 else cR * max (3 - s) 0 / Real.log y) + 6 * CR * s ^ 2 * errMaj lower s * pntE (y ^ (1 / xi y)) / Real.log y

The source term in the form needed for the induction.

theorem IwaniecLinearSieve.TheoremFour.main_sum_add_src_le {cR CR C₁ : ℝ} (hcR : 0 ≤ cR) {lower : Bool} {y s : ℝ} (hcor1 : ∑ p ∈ rosserPrimes lower y (y ^ (1 / s)) with y ^ (1 / xi y) ≤ ↑p, mainMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p)) ≤ (mainMaj lower s - if lower = true then 0 else max (3 - s) 0) / Real.log y + C₁ * s ^ 2 * errMaj lower s * pntE (y ^ (1 / xi y)) / Real.log y) (hsrc : src lower y (y ^ (1 / s)) ≤ (if lower = true then 0 else cR * max (3 - s) 0 / Real.log y) + 6 * CR * s ^ 2 * errMaj lower s * pntE (y ^ (1 / xi y)) / Real.log y) : cR * ∑ p ∈ rosserPrimes lower y (y ^ (1 / s)) with y ^ (1 / xi y) ≤ ↑p, mainMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p)) + src lower y (y ^ (1 / s)) ≤ cR * mainMaj lower s / Real.log y + (cR * C₁ + 6 * CR) * s ^ 2 * errMaj lower s * pntE (y ^ (1 / xi y)) / Real.log y

Corollary 1 and the source estimate together give the full main term: the source restores the upper-sieve correction (3 - s)⁺ subtracted from the prime sum.

Small y

theorem IwaniecLinearSieve.TheoremFour.SLT_mono {a b : ℝ} (hab : a ≤ b) : SLT a ≤ SLT b

theorem IwaniecLinearSieve.TheoremFour.fail_le_exp_SLT (lower : Bool) (r : ℕ) (y z : ℝ) : fail lower r y z ≤ Real.exp (SLT z)

theorem IwaniecLinearSieve.TheoremFour.xi_le_of_le {y Y : ℝ} (hy : 1 < y) (hyY : y ≤ Y) : xi y ≤ Real.log Y / Real.log (Real.log 3) ^ (11 / 5)

theorem IwaniecLinearSieve.TheoremFour.small_y {cR c₇ Y : ℝ} (hcR : 0 < cR) (hY : 1 < Y) (hc₇ : 6 * Real.exp (SLT Y) * Real.log Y ^ 2 / (cR * bigM (Real.log Y / Real.log (Real.log 3) ^ (11 / 5))) ≤ c₇) (r : ℕ) (lower : Bool) {y s : ℝ} (hy : 1 < y) (hyY : y ≤ Y) (hs : sMin lower ≤ s) (hsξ : s ≤ xi y) : fail lower (r + 1) y (y ^ (1 / s)) ≤ cR * (mainMaj lower s / Real.log y + c₇ * (↑(r + 1) / (↑(r + 1) + 1)) * delta s y * errMaj lower s / Real.log y ^ 2)

[I71, (4.8)]: for 1 < y ≤ Y the claim at depth r + 1 holds once c₇ is large in terms of Y.

The small primes: the crude bound against Lemma 9

theorem IwaniecLinearSieve.TheoremFour.crude_le : ∃ (y₁ : ℝ), ∀ y ≥ y₁, ∀ (lower : Bool) (n : ℕ) (s : ℝ), sMin lower ≤ s → s ≤ xi y → fail lower n y (y ^ (1 / xi y)) ≤ delta s y * errMaj lower s / Real.log y ^ 4

[I71, (4.9), (4.10)]: for y ≥ y₁ the depth sums at w = y^{1/ξ} are at most δ(s, y) G(s) / L⁴ for every s ≤ ξ.

The inductive step

theorem IwaniecLinearSieve.TheoremFour.ratio_le {r : ℕ} {ε : ℝ} (hε : ε * (↑r + 1) ^ 2 ≤ 1) : ↑r / (↑r + 1) ≤ ↑(r + 1) / (↑(r + 1) + 1) * (1 - ε)

r/(r+1) ≤ (r+1)/(r+2) · (1 - ε) when ε (r+1)² ≤ 1.

theorem IwaniecLinearSieve.TheoremFour.ratio_le_of_depth {r : ℕ} {L Λ : ℝ} (hL : 0 < L) (hΛ : 0 < Λ) (hdepth : ↑r + 2 ≤ 2 * L / Λ) : ↑r / (↑r + 1) ≤ ↑(r + 1) / (↑(r + 1) + 1) * (1 - Λ ^ 2 / (4 * L ^ 2))

The depth condition supplies the relative gain (log L)²/(4L²) used in [I71, (4.6)]. Here Λ stands for log L; the estimate only needs Λ > 0.

theorem IwaniecLinearSieve.TheoremFour.combine {cR c₇ L D M F cr E T ρ ρ' ε : ℝ} (hF : F ≤ cr + (cR * M / L + E) + cR * c₇ * ρ * T) (hcr : cr ≤ D / L ^ 2) (hE : E ≤ D / L ^ 2) (hT : T ≤ D * (1 + ε / 2)) (hρ : ρ ≤ ρ' * (1 - ε)) (hρ0 : 0 ≤ ρ) (hε0 : 0 ≤ ε) (hεL : 1 / (4 * L ^ 2) ≤ ε) (hρ' : 1 / 2 ≤ ρ') (hc : 32 ≤ cR * c₇) (hD : 0 ≤ D) (hL : 0 < L) : F ≤ cR * M / L + cR * c₇ * ρ' * D

The final bookkeeping of the inductive step ([I71, (4.6)]).

theorem IwaniecLinearSieve.TheoremFour.main_step {cR c₇ CR C₁ C₃ : ℝ} {r : ℕ} (IH : Bound cR c₇ r) (hcR : 0 < cR) (hc₇ : 32 ≤ cR * c₇) (hCR : 0 ≤ CR) (hC₁ : 0 ≤ C₁) (hC₃ : 0 ≤ C₃) {lower : Bool} {y s : ℝ} (hy : 1 < y) (hs : sMin lower ≤ s) (hsξ : s ≤ xi y) (hcor1 : ∑ p ∈ rosserPrimes lower y (y ^ (1 / s)) with y ^ (1 / xi y) ≤ ↑p, mainMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p)) ≤ (mainMaj lower s - if lower = true then 0 else max (3 - s) 0) / Real.log y + C₁ * s ^ 2 * errMaj lower s * pntE (y ^ (1 / xi y)) / Real.log y) (hsrc : src lower y (y ^ (1 / s)) ≤ (if lower = true then 0 else cR * max (3 - s) 0 / Real.log y) + 6 * CR * s ^ 2 * errMaj lower s * pntE (y ^ (1 / xi y)) / Real.log y) (hcor3 : ∑ p ∈ rosserPrimes lower y (y ^ (1 / s)) with y ^ (1 / xi y) ≤ ↑p, delta (Real.log y / Real.log ↑p - 1) (y / ↑p) * errMaj (!lower) (Real.log y / Real.log ↑p - 1) / (↑p * Real.log (y / ↑p) ^ 2) ≤ delta (max s (Real.exp 32)) y * errMaj lower s / Real.log y ^ 2 * (1 + C₃ * xi y ^ 2 * pntE (y ^ (1 / xi y)))) (hcrude : fail lower (r + 1) y (y ^ (1 / xi y)) ≤ delta s y * errMaj lower s / Real.log y ^ 4) (hΛ : 1 ≤ Real.log (Real.log y)) (hδ : 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)) (hK : (cR * C₁ + 6 * CR) * xi y ^ 2 * Real.log y ^ 3 * pntE (y ^ (1 / xi y)) ≤ 1) (hdepth : ¬2 * Real.log y / Real.log (Real.log y) < ↑r + 2) : fail lower (r + 1) y (y ^ (1 / s)) ≤ cR * (mainMaj lower s / Real.log y + c₇ * (↑(r + 1) / (↑(r + 1) + 1)) * delta s y * errMaj lower s / Real.log y ^ 2)

The main case of the inductive step: y large and r + 2 ≤ 2 L / log L. All analytic inputs are hypotheses at the given y, s.

theorem IwaniecLinearSieve.theorem4 {cR CR : ℝ} (hcR : 0 < cR) (hR : ∀ z ≥ 2, |R z * Real.log z - cR| ≤ CR * pntE z) : ∃ (c₇ : ℝ), 0 ≤ c₇ ∧ ∀ (r : ℕ) (lower : Bool) (y s : ℝ), 1 < y → sMin lower ≤ s → s ≤ xi y → fail lower r y (y ^ (1 / s)) ≤ cR * (mainMaj lower s / Real.log y + c₇ * (↑r / (↑r + 1)) * delta s y * errMaj lower s / Real.log y ^ 2)

[I71, Theorem 4] (main terms), for k = 1: if cR, CR are as in R_asymp (|R(z) log z - cR| ≤ CR pntE(z) for z ≥ 2), there is c₇ ≥ 0 such that for all r, both sieves, y > 1 and sMin lower ≤ s ≤ ξ(y),

fail lower r y (y^{1/s}) ≤ cR (M(s)/L + c₇ r/(r+1) δ(s, y) G(s)/L²),

where M = mainMaj lower (f, resp. F + (3 - s)⁺), G = errMaj lower (𝔣, resp. 𝔉), L = log y.