The crude bound for deep terms ([I71, pp. 24, 27])

A failing tuple p₁ > ⋯ > p_l (all < z) of depth l satisfies p₁ ⋯ p_l p_l² ≥ y, so z^{l+2} > y; it contributes R(p_l)/(p₁ ⋯ p_l) ≤ 1/(p₁ ⋯ p_l), and the sum of 1/(p₁ ⋯ p_l) over z > p₁ > ⋯ > p_l is at most (∑_{p<z} 1/p)^l / l!. Hence (fail_le_sum_SLT_pow) fail lower r y z ≤ ∑_{1 ≤ l ≤ r, y < z^{l+2}} SLT(z)^l / l!,

which is [I71]'s Q_{m+1,y}(ξ-1) < ∑_{k > ξ-3} (∑_{p<y} 1/p)^k / k! (with z = y^{1/(ξ-1)}). With the tail estimate sum_pow_div_factorial_le (∑_{l > u} X^l / l! ≤ 2 (e X / u)^u for 2 e X ≤ u) and SLT_le_loglog (SLT z ≤ log log z + C) this gives fail_le_tail: z^{u+2} ≤ y, SLT z ≤ X, 2 e X ≤ u → fail lower r y z ≤ 2 (e X / u)^u = 2 exp (-(u log u) + u log X + u).

For the counts ([I71, p. 27]): elements with l ≥ 2 prime factors (l ≥ 1 for the upper sieve) are < y, and ∑_{d ∈ D, ω(d) = l} 1/d ≤ SLT(z)^l / l!, so #{d ∈ D | ω(d) ≥ k} ≤ y ∑_{k ≤ l ≤ π(z)} SLT(z)^l / l! (card_filter_le_mul_sum); also #{d ∈ D | ω(d) = l} ≤ π(z)^l / l! (card_filter_eq_le_pow_div).

Discrete integration

theorem IwaniecLinearSieve.pow_succ_add_mul_le_add_pow {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (n : ℕ) : a ^ (n + 1) + (↑n + 1) * a ^ n * b ≤ (a + b) ^ (n + 1)

a^{n+1} + (n+1) a^n b ≤ (a + b)^{n+1} for a, b ≥ 0.

theorem IwaniecLinearSieve.sum_pow_sum_lt_mul_le (s : Finset ℕ) {w : ℕ → ℝ} (hw : ∀ p ∈ s, 0 ≤ w p) (n : ℕ) : ∑ p ∈ s, (∑ q ∈ s with q < p, w q) ^ n * w p ≤ (∑ q ∈ s, w q) ^ (n + 1) / (↑n + 1)

Discrete form of ∫ F(t)^n dF(t) ≤ F^{n+1}/(n+1): for weights w ≥ 0 on a finite set of naturals, ∑_{p ∈ s} (∑_{q ∈ s, q < p} w q)^n w p ≤ (∑_{q ∈ s} w q)^{n+1} / (n+1).

theorem IwaniecLinearSieve.sum_SLT_pow_div_le (n : ℕ) (z : ℝ) : ∑ p ∈ primesLT z, SLT ↑p ^ n / ↑p ≤ SLT z ^ (n + 1) / (↑n + 1)

∑_{p < z} SLT(p)^n / p ≤ SLT(z)^{n+1} / (n+1).

theorem IwaniecLinearSieve.sum_SLT_pow_div_factorial_div_le (n : ℕ) (z : ℝ) : ∑ p ∈ primesLT z, SLT ↑p ^ n / ↑n.factorial / ↑p ≤ SLT z ^ (n + 1) / ↑(n + 1).factorial

∑_{p < z} (SLT(p)^n / n!) / p ≤ SLT(z)^{n+1} / (n+1)!.

theorem IwaniecLinearSieve.SLT_nonneg (z : ℝ) : 0 ≤ SLT z

theorem IwaniecLinearSieve.R_le_one (z : ℝ) : R z ≤ 1

The crude bound for fail

theorem IwaniecLinearSieve.fail_le_sum_ite (lower : Bool) (r : ℕ) (y z : ℝ) : fail lower r y z ≤ ∑ l ∈ Finset.range r, if y < z ^ (l + 3) then SLT z ^ (l + 1) / ↑(l + 1).factorial else 0

The crude bound in "shifted" form: depth l + 1 contributes only if y < z^{l+3}.

theorem IwaniecLinearSieve.fail_le_sum_SLT_pow (lower : Bool) (r : ℕ) (y z : ℝ) : fail lower r y z ≤ ∑ l ∈ Finset.Icc 1 r with y < z ^ (l + 2), SLT z ^ l / ↑l.factorial

[I71, p. 24]: the deficits are bounded by the sum of SLT(z)^l / l! over the depths 1 ≤ l ≤ r for which y < z^{l+2}.

Tail estimates

theorem IwaniecLinearSieve.pow_div_factorial_le_pow {X : ℝ} (hX : 0 ≤ X) (k : ℕ) : X ^ k / ↑k.factorial ≤ (Real.exp 1 * X / ↑k) ^ k

X^k / k! ≤ (e X / k)^k.

theorem IwaniecLinearSieve.sum_pow_div_factorial_le {X u : ℝ} (hX : 0 ≤ X) (hu : 0 < u) (h : 2 * Real.exp 1 * X ≤ u) (s : Finset ℕ) (hs : ∀ l ∈ s, u < ↑l) : ∑ l ∈ s, X ^ l / ↑l.factorial ≤ 2 * (Real.exp 1 * X / u) ^ u

[I71, p. 24]: the tail ∑_{l > u} X^l / l! (over any finite set of l > u) is at most 2 (e X / u)^u when 2 e X ≤ u.

theorem IwaniecLinearSieve.exp_one_mul_div_rpow {X u : ℝ} (hX : 0 < X) (hu : 0 < u) : (Real.exp 1 * X / u) ^ u = Real.exp (-(u * Real.log u) + u * Real.log X + u)

(e X / u)^u = exp (-(u log u) + u log X + u).

theorem IwaniecLinearSieve.fail_le_tail {lower : Bool} {r : ℕ} {y z X u : ℝ} (hz : 1 < z) (hu : 0 < u) (hyz : z ^ (u + 2) ≤ y) (hX : SLT z ≤ X) (h : 2 * Real.exp 1 * X ≤ u) : fail lower r y z ≤ 2 * (Real.exp 1 * X / u) ^ u

The crude bound in the form used in [I71, p. 24]: if z^{u+2} ≤ y (i.e. s ≥ u + 2 for z = y^{1/s}), SLT z ≤ X and 2 e X ≤ u, then fail lower r y z ≤ 2 (e X / u)^u.

theorem IwaniecLinearSieve.fail_rpow_le_tail {lower : Bool} {r : ℕ} {y s X : ℝ} (hy : 1 < y) (hs : 2 < s) (hX : SLT (y ^ s⁻¹) ≤ X) (h : 2 * Real.exp 1 * X ≤ s - 2) : fail lower r y (y ^ s⁻¹) ≤ 2 * (Real.exp 1 * X / (s - 2)) ^ (s - 2)

fail_le_tail with z = y^{1/s}: for y > 1, s > 2, SLT (y^{1/s}) ≤ X and 2 e X ≤ s - 2, fail lower r y y^{1/s} ≤ 2 (e X / (s - 2))^{s - 2}.

theorem IwaniecLinearSieve.SLT_le_loglog : ∃ (C : ℝ), ∀ z ≥ 2, SLT z ≤ Real.log (Real.log z) + C

SLT z ≤ log log z + C for z ≥ 2.

Counts

theorem IwaniecLinearSieve.sum_inv_filter_card_primeFactors_eq_le (lower : Bool) (y z : ℝ) (l : ℕ) : ∑ d ∈ rosserSet lower y z with d.primeFactors.card = l, (↑d)⁻¹ ≤ SLT z ^ l / ↑l.factorial

∑_{d ∈ D, ω(d) = l} 1/d ≤ SLT(z)^l / l!.

theorem IwaniecLinearSieve.card_filter_le_mul_sum {lower : Bool} {y z : ℝ} {k : ℕ} (hy : 0 ≤ y) (hk : (if lower = true then 2 else 1) ≤ k) : ↑{d ∈ rosserSet lower y z | k ≤ d.primeFactors.card}.card ≤ y * ∑ l ∈ Finset.Icc k (primesLT z).card, SLT z ^ l / ↑l.factorial

[I71, p. 27]: the number of elements of rosserSet lower y z with at least k prime factors, for k ≥ 2 (k ≥ 1 for the upper sieve), is at most y ∑_{k ≤ l ≤ π(z)} SLT(z)^l / l!.

theorem IwaniecLinearSieve.card_filter_le_tail {lower : Bool} {y z X u : ℝ} {k : ℕ} (hy : 0 ≤ y) (hk : (if lower = true then 2 else 1) ≤ k) (hu : 0 < u) (huk : u < ↑k) (hX : SLT z ≤ X) (h : 2 * Real.exp 1 * X ≤ u) : ↑{d ∈ rosserSet lower y z | k ≤ d.primeFactors.card}.card ≤ 2 * y * (Real.exp 1 * X / u) ^ u

[I71, p. 27]: #{d ∈ D | ω(d) ≥ k} ≤ 2 y (e X / u)^u for u < k, SLT z ≤ X and 2 e X ≤ u, where k ≥ 2 (k ≥ 1 for the upper sieve).

theorem IwaniecLinearSieve.card_filter_eq_le_pow_div (lower : Bool) (y z : ℝ) (l : ℕ) : ↑{d ∈ rosserSet lower y z | d.primeFactors.card = l}.card ≤ ↑(primesLT z).card ^ l / ↑l.factorial

The number of elements of rosserSet lower y z with exactly l prime factors is at most π(z)^l / l!.