Reduction of Jacobsthal's problem to the linear sieve ([I78, §3])

iwaniecBound_of_estimates derives Iwaniec's bound m ≪ (r log r)² for the length m of a run of consecutive integers each divisible by one of r ≥ 2 given primes, from three analytic inputs taken as hypotheses:

• LinearSieveEstimate (proved as linearSieveEstimate): [I71]'s bounds (main term and support size) for Rosser's lower-bound sieve at level y = C₀ z², i.e. (5) and (6) of [I78, Lemma 2];
• R(z) ≫ 1 / log z (Mertens);
• p_r ≪ r log r for the r-th prime.

The proof is [I78, §3]: the shifted sieve (shiftedSieve) with X = m, for which the sifted set is empty, gives m ∏_{q ∈ S} (1 - 1/q) · (∑_{D⁻} μ(d)/d) / R(z) ≤ |D⁻|.

theorem IwaniecLinearSieve.exists_covering_length_le (hL : LinearSieveEstimate) (hR : ∃ c > 0, ∀ z ≥ 2, c / Real.log z ≤ R z) : ∃ (K : ℝ) (z₁ : ℝ), ∀ z ≥ z₁, ∀ (S : Finset ℕ), (∀ p ∈ S, Nat.Prime p) → S.card = (primesLT z).card → ∀ (x : ℤ) (m : ℕ), (∀ k < m, ∃ p ∈ S, ↑p ∣ x + ↑k) → ↑m ≤ K * z ^ 2

From the linear sieve estimate and R(z) ≫ 1 / log z: if π(z) primes cover m consecutive integers, then m ≪ z².

theorem IwaniecLinearSieve.card_primesLT_nth_prime_add_one (n : ℕ) : (primesLT (↑(Nat.nth Nat.Prime n) + 1)).card = n + 1

The primes below p_N + 1, where p_N = Nat.nth Nat.Prime (N - 1) is the N-th prime, are the first N primes.

theorem IwaniecLinearSieve.exists_superset_card_eq {S : Finset ℕ} (hS : ∀ p ∈ S, Nat.Prime p) {N : ℕ} (hN : S.card ≤ N) : ∃ (S' : Finset ℕ), S ⊆ S' ∧ (∀ p ∈ S', Nat.Prime p) ∧ S'.card = N

Any finite set of r ≤ N primes extends to a set of exactly N primes.

theorem IwaniecLinearSieve.iwaniecBound_of_estimates (hL : LinearSieveEstimate) (hR : ∃ c > 0, ∀ z ≥ 2, c / Real.log z ≤ R z) (hp : ∃ (C : ℝ), ∀ r ≥ 2, ↑(Nat.nth Nat.Prime (r - 1)) ≤ C * ↑r * Real.log ↑r) : ∃ (C : ℝ), ∀ (S : Finset ℕ), (∀ p ∈ S, Nat.Prime p) → 2 ≤ S.card → ∀ (x : ℤ) (m : ℕ), (∀ k < m, ∃ p ∈ S, ↑p ∣ x + ↑k) → ↑m ≤ C * (↑S.card * Real.log ↑S.card) ^ 2

Iwaniec's bound for Jacobsthal's function ([I78, Corollary]), assuming the linear sieve estimate of [I71], the lower bound R(z) ≫ 1 / log z, and the bound p_r ≪ r log r for the r-th prime: if r ≥ 2 primes cover m consecutive integers, then m ≪ (r log r)².

Given S with #S = r, we enlarge S to N = N₀ r primes (so that z = p_N + 1 ≥ z₀) and apply exists_covering_length_le with z = p_N + 1, so that primesLT z consists of the first N primes.