Auxiliary facts for [I71, Theorem 4]

• the telescoping identity ∑_{a ≤ p < b} R(p)/p = R(a) - R(b) (from R_eq), and the bound for the depth-one source term of the upper sieve via R_asymp;
• monotonicity of δ(s, y) in s, and δ(max s s₀, y) ≤ δ(s₀, y) δ(s, y);
• the inner level of the recursion: (y/p)^{1/(t_p - 1)} = p, the domain condition sMin (!lower) ≤ t_p - 1, and t_p - 1 ≤ ξ(y/p) for p ≥ y^{1/ξ(y)};
• the splitting of fail lower (r+1) y z at w ≤ z.

The depth-one source term

theorem IwaniecLinearSieve.TheoremFour.sum_R_div_eq {a b : ℝ} (hab : a ≤ b) : ∑ p ∈ primesLT b with a ≤ ↑p, R ↑p / ↑p = R a - R b

Telescoping: ∑_{a ≤ p < b} R(p)/p = R(a) - R(b) for a ≤ b.

noncomputable def IwaniecLinearSieve.TheoremFour.src (lower : Bool) (y z : ℝ) : ℝ

The depth-one source term of fail false: the primes p < z with p³ ≥ y (none for the lower sieve).

Equations

• IwaniecLinearSieve.TheoremFour.src lower y z = if lower = true then 0 else ∑ p ∈ IwaniecLinearSieve.primesLT z with ¬↑p ^ 3 < y, IwaniecLinearSieve.R ↑p / ↑p

theorem IwaniecLinearSieve.TheoremFour.src_nonneg (lower : Bool) (y z : ℝ) : 0 ≤ src lower y z

theorem IwaniecLinearSieve.TheoremFour.fail_succ_eq (lower : Bool) (r : ℕ) (y z : ℝ) : fail lower (r + 1) y z = ∑ p ∈ rosserPrimes lower y z, fail (!lower) r (y / ↑p) ↑p / ↑p + src lower y z

theorem IwaniecLinearSieve.TheoremFour.not_cube_lt_iff {y x : ℝ} (hy : 0 ≤ y) (hx : 0 ≤ x) : ¬x ^ 3 < y ↔ y ^ (1 / 3) ≤ x

¬ p³ < y ↔ y^{1/3} ≤ p.

theorem IwaniecLinearSieve.TheoremFour.src_le {cR CR : ℝ} (hR : ∀ z ≥ 2, |R z * Real.log z - cR| ≤ CR * pntE z) {lower : Bool} {y s w : ℝ} (hy : 1 < y) (hs : 1 ≤ s) (hw : 2 ≤ w) (hwz : w ≤ y ^ (1 / s)) (hw3 : w ≤ y ^ (1 / 3)) : src lower y (y ^ (1 / s)) ≤ (if lower = true then 0 else cR * max (3 - s) 0 / Real.log y) + 6 * CR * pntE w / Real.log y

The source term for z = y^{1/s}: R(y^{1/3}) - R(y^{1/s}) ≤ cR (3 - s)⁺ / L + 6 C_R pntE(w) / L for any w ≥ 2 below y^{1/s} and y^{1/3} (and 0 for the lower sieve).

The compensation factor δ

theorem IwaniecLinearSieve.TheoremFour.one_le_delta {s : ℝ} (hs : 1 ≤ s) (y : ℝ) : 1 ≤ delta s y

theorem IwaniecLinearSieve.TheoremFour.delta_le_delta {s s' : ℝ} (hs : 1 ≤ s) (hss' : s ≤ s') (y : ℝ) : delta s y ≤ delta s' y

theorem IwaniecLinearSieve.TheoremFour.delta_max_le {s a : ℝ} (hs : 1 ≤ s) (ha : 1 ≤ a) (y : ℝ) : delta (max s a) y ≤ delta a y * delta s y

The inner level of the recursion

theorem IwaniecLinearSieve.TheoremFour.rpow_inner_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 for 1 < p < y, t_p = log y / log p.

theorem IwaniecLinearSieve.TheoremFour.lt_div_log_of_lt_rpow {y s : ℝ} {p : ℕ} (hy : 1 < y) (hs : 0 < s) (hp : 1 < p) (hpz : ↑p < y ^ (1 / s)) : s < Real.log y / Real.log ↑p

p < y^{1/s} ⇒ s < t_p.

theorem IwaniecLinearSieve.TheoremFour.prime_lt_of_mem_rosserPrimes {lower : Bool} {y s : ℝ} {p : ℕ} (hy : 1 < y) (hs : 1 ≤ s) (hp : p ∈ rosserPrimes lower y (y ^ (1 / s))) : ↑p < y

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

The inner parameter t_p - 1 lies in the domain of !lower.

theorem IwaniecLinearSieve.TheoremFour.one_lt_log_three_mul {x : ℝ} (hx : 1 ≤ x) : 1 < Real.log (3 * x)

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

log (y^{1/ξ(y)}) = (log log 3y)^{11/5}.

theorem IwaniecLinearSieve.TheoremFour.inner_le_xi {y : ℝ} {p : ℕ} (hy : 1 < y) (hp : 1 < p) (hpy : ↑p < y) (hw : y ^ (1 / xi y) ≤ ↑p) : Real.log y / Real.log ↑p - 1 ≤ xi (y / ↑p)

For y^{1/ξ(y)} ≤ p < y, the inner parameter satisfies t_p - 1 ≤ ξ(y/p).

Splitting the prime sum

theorem IwaniecLinearSieve.TheoremFour.rosserPrimes_filter_lt {lower : Bool} {y z w : ℝ} (hwz : w ≤ z) : {p ∈ rosserPrimes lower y z | ¬w ≤ ↑p} = rosserPrimes lower y w

theorem IwaniecLinearSieve.TheoremFour.fail_succ_le_split (lower : Bool) (r : ℕ) {y z w : ℝ} (hwz : w ≤ z) : fail lower (r + 1) y z ≤ fail lower (r + 1) y w + ∑ p ∈ rosserPrimes lower y z with w ≤ ↑p, fail (!lower) r (y / ↑p) ↑p / ↑p + src lower y z

fail lower (r+1) y z ≤ fail lower (r+1) y w + ∑_{w ≤ p} (inner terms) + source.