Iwaniec's shifted sieve ([I78, Lemma 1])

Let S be any set of r = π(z) primes, and match S with the primes below z in increasing order, l : S → primesLT z, so that l(q) ≤ q. Rosser's lower-bound weights λ_d = μ(d) on d ∈ D⁻ (supported on divisors of P(z)) are pulled back along l to divisors of Q = ∏_{q ∈ S} q. Writing divisors of squarefree numbers as sets of primes, the weights are rosserWeight y z A for A ⊆ primesLT z.

• sum_powerset_div_prod: ∑_{A ⊆ T} w(A)/∏_A g = ∏_T (1 - 1/g) ∑_{B ⊆ T} σ(B)/∏_B (g - 1).
• prod_mul_sum_div_le_sum: the comparison of main terms under condition (−).
• shiftedSieve: [I78, Lemma 1] for X consecutive integers.
• R_le_prod_of_card_eq: R(z) ≤ ∏_{q ∈ S} (1 - 1/q).

Matching an arbitrary set of primes with the first primes

theorem IwaniecLinearSieve.orderEmbOfFin_le_orderEmbOfFin {T S : Finset ℕ} {r : ℕ} (hT : T.card = r) (hS : S.card = r) (hdown : ∀ q ∈ S, ∀ t ∈ T, q < t → q ∈ T) (i : Fin r) : (T.orderEmbOfFin hT) i ≤ (S.orderEmbOfFin hS) i

If every element of S lying below some element of T belongs to T (e.g. T is the set of the first r primes and S is any set of primes), then the i-th element of T is at most the i-th element of S.

theorem IwaniecLinearSieve.exists_bijOn_le {T S : Finset ℕ} (hcard : S.card = T.card) (hdown : ∀ q ∈ S, ∀ t ∈ T, q < t → q ∈ T) : ∃ (e : ℕ → ℕ), Set.BijOn e ↑T ↑S ∧ ∀ p ∈ T, p ≤ e p

The order-preserving bijection between two finite sets of the same size moves every element of T upwards, provided every element of S below an element of T lies in T.

Möbius inversion over subsets

theorem IwaniecLinearSieve.sum_powerset_filter_superset_prod {T A : Finset ℕ} (hA : A ⊆ T) (h : ℕ → ℝ) : ∑ B ∈ T.powerset with A ⊆ B, ∏ p ∈ B, h p = (∏ p ∈ A, h p) * ∏ p ∈ T \ A, (1 + h p)

theorem IwaniecLinearSieve.sum_powerset_div_prod (T : Finset ℕ) (g : ℕ → ℝ) (hg : ∀ p ∈ T, g p ≠ 0 ∧ g p ≠ 1) (w : Finset ℕ → ℝ) : ∑ A ∈ T.powerset, w A / ∏ p ∈ A, g p = (∏ p ∈ T, (1 - (g p)⁻¹)) * ∑ B ∈ T.powerset, (∑ A ∈ B.powerset, w A) / ∏ p ∈ B, (g p - 1)

The identity behind [I78, Lemma 1]: for weights w on the subsets of T (i.e. on the divisors of ∏_{p ∈ T} p) with partial sums σ(B) = ∑_{A ⊆ B} w(A), ∑_{A ⊆ T} w(A) / ∏_{p ∈ A} g(p) = ∏_{p ∈ T} (1 - 1/g(p)) ∑_{B ⊆ T} σ(B) / ∏_{p ∈ B} (g(p) - 1).

theorem IwaniecLinearSieve.prod_mul_sum_div_le_sum (T : Finset ℕ) (f g : ℕ → ℝ) (hg : ∀ p ∈ T, 1 < g p) (hgf : ∀ p ∈ T, g p ≤ f p) (w : Finset ℕ → ℝ) (hw : ∀ B ⊆ T, B.Nonempty → ∑ A ∈ B.powerset, w A ≤ 0) : (∏ p ∈ T, (1 - (f p)⁻¹)) * ((∑ A ∈ T.powerset, w A / ∏ p ∈ A, g p) / ∏ p ∈ T, (1 - (g p)⁻¹)) ≤ ∑ A ∈ T.powerset, w A / ∏ p ∈ A, f p

The main-term comparison in [I78, Lemma 1]: if the partial sums of w are ≤ 0 on nonempty sets ("condition (−)") and 1 < g ≤ f on T, then ∏ (1 - 1/f) · (∑_A w(A) / ∏_A g) / ∏ (1 - 1/g) ≤ ∑_A w(A) / ∏_A f.

Rosser's weights on subsets of the primes below z

theorem IwaniecLinearSieve.sum_rosserSet_eq_sum_powerset {M : Type u_1} [AddCommMonoid M] (lower : Bool) (y z : ℝ) (F : Finset ℕ → M) : ∑ d ∈ rosserSet lower y z, F d.primeFactors = ∑ A ∈ (primesLT z).powerset, if ∏ p ∈ A, p ∈ rosserSet lower y z then F A else 0

Sums over rosserSet as sums over sets of primes below z.

theorem IwaniecLinearSieve.sum_rosserSet_eq_sum_powerset' {M : Type u_1} [AddCommMonoid M] (lower : Bool) (y z : ℝ) (G : ℕ → M) : ∑ d ∈ rosserSet lower y z, G d = ∑ A ∈ (primesLT z).powerset, if ∏ p ∈ A, p ∈ rosserSet lower y z then G (∏ p ∈ A, p) else 0

noncomputable def IwaniecLinearSieve.rosserWeight (y z : ℝ) (A : Finset ℕ) : ℝ

λ_A = μ(∏_{p ∈ A} p) if ∏_{p ∈ A} p ∈ D⁻, and 0 otherwise.

Equations

• IwaniecLinearSieve.rosserWeight y z A = if ∏ p ∈ A, p ∈ IwaniecLinearSieve.rosserSet true y z then ↑(ArithmeticFunction.moebius (∏ p ∈ A, p)) else 0

theorem IwaniecLinearSieve.sum_moebius_rosserSet_eq (y z : ℝ) (F : ℕ → ℝ) : ∑ d ∈ rosserSet true y z, ↑(ArithmeticFunction.moebius d) * F d = ∑ A ∈ (primesLT z).powerset, rosserWeight y z A * F (∏ p ∈ A, p)

theorem IwaniecLinearSieve.rosserMain_eq_sum_rosserWeight (y z : ℝ) : rosserMain true y z = ∑ A ∈ (primesLT z).powerset, rosserWeight y z A / ∏ p ∈ A, ↑p

theorem IwaniecLinearSieve.sum_abs_rosserWeight_le (y z : ℝ) : ∑ A ∈ (primesLT z).powerset, |rosserWeight y z A| ≤ ↑(rosserSet true y z).card

theorem IwaniecLinearSieve.prod_dvd_prod_iff_subset {A B : Finset ℕ} (hA : ∀ p ∈ A, Nat.Prime p) (hB : ∀ p ∈ B, Nat.Prime p) : ∏ p ∈ A, p ∣ ∏ p ∈ B, p ↔ A ⊆ B

theorem IwaniecLinearSieve.sum_powerset_rosserWeight_le (y : ℝ) {z : ℝ} {B : Finset ℕ} (hB : B ⊆ primesLT z) : ∑ A ∈ B.powerset, rosserWeight y z A ≤ if B = ∅ then 1 else 0

The sieve property in terms of subsets ("condition (−)" of [I78, Lemma 1]): ∑_{A ⊆ B} λ_A ≤ [B = ∅].

Counting multiples in an interval

theorem IwaniecLinearSieve.abs_card_filter_dvd_sub_le (x : ℤ) (X : ℕ) {d : ℕ} (hd : 0 < d) : |↑{k ∈ Finset.range X | ↑d ∣ x + ↑k}.card - ↑X / ↑d| ≤ 1

|#{k < X : d ∣ x + k} - X / d| ≤ 1.

The shifted sieve

theorem IwaniecLinearSieve.shiftedSieve_of_bijOn {z : ℝ} (y : ℝ) {S : Finset ℕ} {e : ℕ → ℕ} (he : Set.BijOn e ↑(primesLT z) ↑S) (hle : ∀ p ∈ primesLT z, p ≤ e p) (hS : ∀ q ∈ S, Nat.Prime q) (x : ℤ) (X : ℕ) : (↑X * ∏ q ∈ S, (1 - (↑q)⁻¹)) * (rosserMain true y z / R z) - ↑(rosserSet true y z).card ≤ ↑{k ∈ Finset.range X | ∀ q ∈ S, ¬↑q ∣ x + ↑k}.card

[I78, Lemma 1] for an interval of X consecutive integers, with an explicit matching e of the primes below z with S such that p ≤ e p.

theorem IwaniecLinearSieve.exists_bijOn_primesLT_le {z : ℝ} {S : Finset ℕ} (hS : ∀ q ∈ S, Nat.Prime q) (hcard : S.card = (primesLT z).card) : ∃ (e : ℕ → ℕ), Set.BijOn e ↑(primesLT z) ↑S ∧ ∀ p ∈ primesLT z, p ≤ e p

Any π(z) primes can be matched with the primes below z so that each prime below z is matched with a prime at least as large.

theorem IwaniecLinearSieve.shiftedSieve {z : ℝ} (y : ℝ) {S : Finset ℕ} (hS : ∀ q ∈ S, Nat.Prime q) (hcard : S.card = (primesLT z).card) (x : ℤ) (X : ℕ) : (↑X * ∏ q ∈ S, (1 - (↑q)⁻¹)) * (rosserMain true y z / R z) - ↑(rosserSet true y z).card ≤ ↑{k ∈ Finset.range X | ∀ q ∈ S, ¬↑q ∣ x + ↑k}.card

[I78, Lemma 1] (the shifted sieve) for an interval of X consecutive integers x + k, 0 ≤ k < X, sifted by an arbitrary set S of π(z) primes, with Rosser's lower-bound weights: #{k < X : (x + k, ∏_{q ∈ S} q) = 1} ≥ X ∏_{q ∈ S} (1 - 1/q) · (∑_{d ∈ D⁻} μ(d)/d) / R(z) - |D⁻|.

theorem IwaniecLinearSieve.R_le_prod_of_card_eq {z : ℝ} {S : Finset ℕ} (hS : ∀ q ∈ S, Nat.Prime q) (hcard : S.card = (primesLT z).card) : R z ≤ ∏ q ∈ S, (1 - (↑q)⁻¹)

R(z) ≤ ∏_{q ∈ S} (1 - 1/q) for any set S of π(z) primes.