[I71, Theorem 5]: the size of the support of the Rosser weights

For y > 1, sMin lower ≤ s ≤ ξ(y) and every depth r, #{d ∈ rosserSet lower y y^{1/s} | ω(d) ≤ r} ≤ c₇ · (r+1)/(r+2) · δ(s, y) · G(s) · y / log² y

(theorem5), where G = errMaj lower (𝔣 for the lower sieve, 𝔉 for the upper sieve). This is [I71, (4.11)] with the depth shifted by one (A_{r,y} there counts r + 1 levels of the recursion, whence r/(r+1) and G_{r+1}); with our recursion (card_filter_rosserSet_succ) the count at flag lower is compared with errMaj lower. Consequence (card_rosserSet_le): #(rosserSet true y y^{1/s}) ≪ y / log² y uniformly for s ∈ [2, 3].

The proof follows [I71, pp. 26–27], by induction on r for both flags at once:

• y < c₈: the count is at most y (card_rosserSet_le), and c₇ is chosen large;
• y ≥ c₈ and r + 3 > 2 log y / log log y: the count does not change from depth r to r + 1 (exists_card_filter_rosserSet_add_eq);
• otherwise Lemma 17 is split at w = y^{1/(ξ-1)}: the primes p ≥ w are handled by the induction hypothesis at (y/p, t_p - 1) and Corollary 3, the primes p < w give at most #(rosserSet lower y w), which is small by the crude count (exists_card_small). The losses (Corollary 3's factor 1 + C ξ² pntE(y^{1/ξ}), δ(max s s₀) ≤ δ(s) δ(s₀), the crude part) are absorbed by (r+2)/(r+3) - (r+1)/(r+2) ≥ (log log y)² / (4 log² y).

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

The statement of Theorem 5 at depth r with constant c₇.

Equations

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

The inner level

Theorems 4 and 5 use the same inner-parameter estimates. These wrappers retain the Theorem 5 statements while sharing the proofs from TheoremFour.

theorem IwaniecLinearSieve.TheoremFive.rosserPrimes_facts {lower : Bool} {y s : ℝ} {p : ℕ} (hy : 1 < y) (hs : sMin lower ≤ s) (hp : p ∈ rosserPrimes lower y (y ^ (1 / s))) : 1 < p ∧ ↑p < y ∧ (sMin !lower) ≤ Real.log y / Real.log ↑p - 1

For p ∈ rosserPrimes lower y y^{1/s}: p < y, and the inner parameter t_p - 1 is in the domain of the opposite flag.

theorem IwaniecLinearSieve.TheoremFive.sub_one_le_xi_div {y : ℝ} {p : ℕ} (hy : 1 < y) (hp : 1 < p) (hpy : ↑p < y) (ht : Real.log y / Real.log ↑p ≤ xi y) : Real.log y / Real.log ↑p - 1 ≤ xi (y / ↑p)

t - 1 ≤ ξ(y/p) for t = t_p ≤ ξ(y), 1 < p < y.

theorem IwaniecLinearSieve.TheoremFive.rpow_inv_sub_one_eq {y : ℝ} {p : ℕ} (hp : 1 < p) (hpy : ↑p < y) : (y / ↑p) ^ (1 / (Real.log y / Real.log ↑p - 1)) = ↑p

(y/p)^{1/(t_p - 1)} = p.

theorem IwaniecLinearSieve.TheoremFive.inner_le {c₇ : ℝ} {r : ℕ} (ih : Bound c₇ r) {lower : Bool} {y s : ℝ} (hy : 1 < y) (hs : sMin lower ≤ s) {p : ℕ} (hp : p ∈ rosserPrimes lower y (y ^ (1 / s))) (ht : Real.log y / Real.log ↑p ≤ xi y) : ↑{d ∈ rosserSet (!lower) (y / ↑p) ↑p | d.primeFactors.card ≤ r}.card ≤ c₇ * ((↑r + 1) / (↑r + 2)) * y * (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), for t_p ≤ ξ(y).

theorem IwaniecLinearSieve.TheoremFive.sum_inner_le {c₇ : ℝ} (hc₇ : 0 ≤ c₇) {r : ℕ} (ih : Bound c₇ r) {lower : Bool} {y s : ℝ} (hy : 1 < y) (hs : sMin lower ≤ s) (hξ : 1 < xi y) : ∑ p ∈ rosserPrimes lower y (y ^ (1 / s)) with y ^ (1 / (xi y - 1)) ≤ ↑p, ↑{d ∈ rosserSet (!lower) (y / ↑p) ↑p | d.primeFactors.card ≤ r}.card ≤ c₇ * ((↑r + 1) / (↑r + 2)) * y * ∑ 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)

Sum the inner induction bounds over p ≥ y^{1/(ξ-1)}, then enlarge the prime range to p ≥ y^{1/ξ} so that Corollary 3 applies.

Closing the induction

theorem IwaniecLinearSieve.TheoremFive.delta_max_le {s s₀ : ℝ} (hs : 1 ≤ s) (hs₀ : 1 ≤ s₀) (y : ℝ) : delta (max s s₀) y ≤ delta s y * delta s₀ y

theorem IwaniecLinearSieve.TheoremFive.gap_le {r : ℕ} {L ℓ : ℝ} (hL : 0 < L) (hℓ : 0 < ℓ) (h : ↑r + 3 ≤ 2 * L / ℓ) : 2 * (ℓ ^ 2 / (8 * L ^ 2)) ≤ (↑r + 1 + 1) / (↑r + 1 + 2) - (↑r + 1) / (↑r + 2)

The gain from depth r to r + 1: (r+2)/(r+3) - (r+1)/(r+2) ≥ ℓ²/(4L²) when r + 3 ≤ 2L/ℓ.

theorem IwaniecLinearSieve.TheoremFive.close_step {c₇ φ φ' Q X ε : ℝ} (hc₇ : 1 ≤ c₇) (hQ : 0 ≤ Q) (hφ1 : φ ≤ 1) (hX0 : 0 ≤ X) (hX : X ≤ ε) (hgap : 2 * ε ≤ φ' - φ) : Q * ε + c₇ * φ * Q * (1 + X) ≤ c₇ * φ' * Q

The final algebra of the inductive step.

theorem IwaniecLinearSieve.TheoremFive.step_main {c₇ C : ℝ} (hc₇ : 1 ≤ c₇) {r : ℕ} (ih : Bound c₇ r) {lower : Bool} {y s : ℝ} (hy : 1 < y) (hs : sMin lower ≤ s) (hξ32 : Real.exp 32 ≤ xi y) (hsmall : 1 + ↑(rosserSet lower y (y ^ (1 / (xi y - 1)))).card ≤ delta s y * errMaj lower s * y / (8 * Real.log y ^ 4)) (hcor : ∑ 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)))) (hC : 0 ≤ C) (hslack : 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)) (hℓ : 1 ≤ Real.log (Real.log y)) (hmain : ↑r + 3 ≤ 2 * Real.log y / Real.log (Real.log y)) : ↑{d ∈ rosserSet lower y (y ^ (1 / s)) | d.primeFactors.card ≤ r + 1}.card ≤ c₇ * ((↑(r + 1) + 1) / (↑(r + 1) + 2)) * delta s y * errMaj lower s * y / Real.log y ^ 2

The main case of the inductive step ([I71, p. 27]): y large and r + 3 ≤ 2 log y / log log y. The hypotheses are the large-y facts: the crude count (exists_card_small), Corollary 3 (cor3_xi) and the slack (exists_slack).

The small-y case

theorem IwaniecLinearSieve.TheoremFive.xi_le_of_lt {y c₈ : ℝ} (hy : 1 < y) (hyc : y < c₈) : xi y ≤ Real.log c₈ / Real.log (Real.log 3) ^ (11 / 5)

ξ(y) ≤ log c₈ / (log log 3)^{11/5} for 1 < y < c₈.

theorem IwaniecLinearSieve.TheoremFive.small_le {c₈ c₇ : ℝ} (hc₇ : 2 * Real.log c₈ ^ 2 / min (errMaj true (Real.log c₈ / Real.log (Real.log 3) ^ (11 / 5))) (errMaj false (Real.log c₈ / Real.log (Real.log 3) ^ (11 / 5))) ≤ c₇) (r : ℕ) (lower : Bool) {y s : ℝ} (hy : 1 < y) (hyc : y < c₈) (hs : sMin lower ≤ s) (hsξ : s ≤ xi y) : ↑{d ∈ rosserSet lower y (y ^ (1 / s)) | d.primeFactors.card ≤ r}.card ≤ c₇ * ((↑r + 1) / (↑r + 2)) * delta s y * errMaj lower s * y / Real.log y ^ 2

For 1 < y < c₈ the count is at most y, which is at most the bound once c₇ ≥ 2 log² c₈ / min (𝔣(Ξ), 𝔉(Ξ)) with Ξ = log c₈ / (log log 3)^{11/5}.

Theorem 5

theorem IwaniecLinearSieve.TheoremFive.exists_bound : ∃ (c₇ : ℝ), 1 ≤ c₇ ∧ ∀ (r : ℕ), Bound c₇ r

theorem IwaniecLinearSieve.theorem5 : ∃ (c₇ : ℝ), 0 ≤ c₇ ∧ ∀ (r : ℕ) (lower : Bool) (y s : ℝ), 1 < y → sMin lower ≤ s → s ≤ xi y → ↑{d ∈ rosserSet lower y (y ^ (1 / s)) | d.primeFactors.card ≤ r}.card ≤ c₇ * ((↑r + 1) / (↑r + 2)) * delta s y * errMaj lower s * y / Real.log y ^ 2

[I71, Theorem 5] (in the indexing of our recursion): there is c₇ such that for all depths r, both sieves, y > 1 and sMin lower ≤ s ≤ ξ(y), the number of elements of rosserSet lower y y^{1/s} with at most r prime factors is at most c₇ (r+1)/(r+2) δ(s, y) G(s) y / log² y, with G = errMaj lower (𝔣 or 𝔉).

theorem IwaniecLinearSieve.delta_le_of_le_three {s y : ℝ} (hs1 : 1 ≤ s) (hs3 : s ≤ 3) (hy : 1 ≤ Real.log y) : delta s y ≤ (1 + 9 * Real.log 3 ^ 5) ^ 15

δ(s, y) ≤ (1 + 9 log⁵ 3)^{15} for 1 ≤ s ≤ 3 and log y ≥ 1.

theorem IwaniecLinearSieve.theorem5_card_rosserSet_le : ∃ (K : ℝ) (y₀ : ℝ), ∀ y ≥ y₀, ∀ s ∈ Set.Icc 2 3, ↑(rosserSet true y (y ^ (1 / s))).card ≤ K * y / Real.log y ^ 2

The consequence of Theorem 5 used for LinearSieveEstimate: the lower-bound sieve support has #(rosserSet true y y^{1/s}) ≪ y / log² y uniformly for 2 ≤ s ≤ 3.