Import Iwaniec's linear sieve and Jacobsthal bound

LeanPool/IwaniecLinearSieve.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+
+module
+
+public import LeanPool.IwaniecLinearSieve.Jacobsthal
+
+/-!
+# Iwaniec's linear sieve and Jacobsthal's bound
+
+Source: doi:10.1515/dema-1978-0121, url:https://github.com/jasondavies/iwaniec-linear-sieve/tree/c8d01549d2ae640b36ec198c1f0f6495f1b036cf
+Authors: Jason Davies, PrimeNumberTheoremAnd contributors
+Status: verified
+Main declarations: `IwaniecLinearSieve.iwaniecBound`
+Tags: analytic-number-theory, sieve-theory, jacobsthal-function, prime-number-theorem
+MSC: 11N35, 11N36, 11N25
+-/

LeanPool/IwaniecLinearSieve/Basic.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+
+module
+
+public import LeanPool.IwaniecLinearSieve.Definitions
+import Mathlib.NumberTheory.Chebyshev
+
+/-!
+# Shared notation
+
+Iwaniec works with primes below a real bound `z`. For `p : ℕ` and `z : ℝ` we have `p < z` iff
+`p < ⌈z⌉₊`, so the primes below `z` are `Nat.primesBelow ⌈z⌉₊`.
+-/
+
+@[expose] public section
+
+open Real
+
+namespace IwaniecLinearSieve
+
+/-- `P(z) = ∏_{p < z} p`. -/
+noncomputable def primorialLT (z : ℝ) : ℕ := ∏ p ∈ primesLT z, p
+
+/-- Iwaniec's `R(z) = ∏_{p < z} (1 - 1/p)` (his `R_k` with `k = 1`). -/
+noncomputable def R (z : ℝ) : ℝ := ∏ p ∈ primesLT z, (1 - (p : ℝ)⁻¹)
+
+theorem mem_primesLT {z : ℝ} {p : ℕ} : p ∈ primesLT z ↔ p.Prime ∧ (p : ℝ) < z := by
+  simp [primesLT, Nat.mem_primesBelow, Nat.lt_ceil, and_comm]
+
+theorem R_nonneg (z : ℝ) : 0 ≤ R z :=
+  Finset.prod_nonneg fun p hp ↦ sub_nonneg.2 <| inv_le_one_of_one_le₀ <| by
+    exact_mod_cast (mem_primesLT.1 hp).1.one_lt.le
+
+theorem R_pos (z : ℝ) : 0 < R z :=
+  Finset.prod_pos fun p hp ↦ sub_pos.2 <| inv_lt_one_of_one_lt₀ <| by
+    exact_mod_cast (mem_primesLT.1 hp).1.one_lt
+
+end IwaniecLinearSieve

LeanPool/IwaniecLinearSieve/Definitions.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+
+module
+
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
+public import Mathlib.NumberTheory.PrimeCounting
+import Mathlib.NumberTheory.Chebyshev
+
+/-!
+# The definitions in the advertised statements
+
+Shared definitions of sifted sets, sieve functions and delay-equation majorants.
+Their analytic and combinatorial properties are proved in the modules below.
+-/
+
+@[expose] public section
+
+open Real Finset
+
+namespace IwaniecLinearSieve
+
+/-! ## Sifted sets ([I71, §1]) -/
+
+/-- The primes `p < z`. -/
+noncomputable def primesLT (z : ℝ) : Finset ℕ := Nat.primesBelow ⌈z⌉₊
+
+/-- The primes `p < z` with `p ∤ k`. -/
+noncomputable def primesLTk (k : ℕ) (z : ℝ) : Finset ℕ := (primesLT z).filter fun p ↦ ¬ p ∣ k
+
+/-- Iwaniec's `R_k(z) = ∏_{p < z, p ∤ k} (1 - 1/p)`. -/
+noncomputable def Rk (k : ℕ) (z : ℝ) : ℝ := ∏ p ∈ primesLTk k z, (1 - (p : ℝ)⁻¹)
+
+/-- Iwaniec's `A_k(M; z)`: the number of terms of `M` not divisible by any prime `p < z`
+with `p ∤ k`. -/
+noncomputable def siftedCount (k : ℕ) (M : Multiset ℤ) (z : ℝ) : ℕ :=
+  M.countP fun a ↦ ∀ p ∈ primesLTk k z, ¬ (p : ℤ) ∣ a
+
+/-- Iwaniec's `|M_d|`: the number of terms of `M` divisible by `d`. -/
+def multiplesCount (M : Multiset ℤ) (d : ℕ) : ℕ := M.countP fun a ↦ (d : ℤ) ∣ a
+
+/-! ## The sieve functions `f` and `F` ([I71, §3, (3.1)–(3.7)]) -/
+
+/-- The formula `3 log (3 / (s - 1)) + s - 4` for `g₂` on `[2, 4]`. -/
+noncomputable def gTwoFormula (s : ℝ) : ℝ := 3 * log (3 / (s - 1)) + s - 4
+
+/-- Left end of the domain of `g i` in [I71]: `2` for even `i`, `3` for odd `i`. -/
+noncomputable def gLower (i : ℕ) : ℝ := if Even i then 2 else 3
+
+/-- The kernel `t ↦ h (t - 1) / (t - 1)`, with the denominator replaced by `max (t - 1) 1` so that
+it is continuous on `ℝ` whenever `h` is. It agrees with `h (t - 1) / (t - 1)` for `t ≥ 2`. -/
+noncomputable def shiftKernel (h : ℝ → ℝ) (t : ℝ) : ℝ := h (t - 1) / max (t - 1) 1
+
+/-- Iwaniec's functions `g_n` of [I71, (3.1)–(3.3)], extended to all of `ℝ`:
+`g₂(s) = 3 log (3 / (s - 1)) + s - 4` on `[2, 4]` and `0` for `s ≥ 4`, and
+`g_{n+1}(s) = ∫_s^∞ g_n(t - 1) / (t - 1) dt` for `s` at least `gLower (n + 1)`.
+Outside the domains of [I71] the argument is clamped: the even functions are constant on
+`s ≤ 2`, the odd ones on `s ≤ 3`, and `g 0 = g 1 = 0`. The upper limit `n + 5 = (n + 3) + 2`
+of the integral can replace `∞` because `g (n + 2) s = 0` for `s ≥ n + 4`. -/
+noncomputable def g : ℕ → ℝ → ℝ
+  | 0, _ => 0
+  | 1, _ => 0
+  | 2, s => gTwoFormula (max 2 (min s 4))
+  | n + 3, s => ∫ t in max s (gLower (n + 3))..((n : ℝ) + 5), shiftKernel (g (n + 2)) t
+
+/-- Iwaniec's `f(s) = Σ_{i ≥ 1} g_{2i}(s)` [I71, (3.6)]; constant (`= f(2) = 2`) for `s ≤ 2`. -/
+noncomputable def fSieve (s : ℝ) : ℝ := ∑' n : ℕ, g (2 * n + 2) s
+
+/-- Iwaniec's `F(s) = Σ_{i ≥ 1} g_{2i+1}(s)` [I71, (3.7)]; constant (`= F(3)`) for `s ≤ 3`. -/
+noncomputable def FSieve (s : ℝ) : ℝ := ∑' n : ℕ, g (2 * n + 3) s
+
+/-! ## The function `𝔐` ([I71, §3, Definition]) -/
+
+namespace Delay
+
+/-- One Picard-type step: `y₀` up to `3`, then integrate `k x * y (x - 1)` from `3`. -/
+noncomputable def step (k y₀ y : ℝ → ℝ) (s : ℝ) : ℝ :=
+  y₀ (min s 3) + ∫ x in (3 : ℝ)..max s 3, k x * y (x - 1)
+
+/-- The iterates of `step`; the `n`-th one is correct on `(-∞, n + 3]`. -/
+noncomputable def iter (k y₀ : ℝ → ℝ) : ℕ → ℝ → ℝ
+  | 0 => y₀
+  | n + 1 => step k y₀ (iter k y₀ n)
+
+/-- The solution `y` of the delay equation `y s = y₀ s` for `s ≤ 3` and
+`y s = y₀ 3 + ∫ x in 3..s, k x * y (x - 1)` for `s ≥ 3`. -/
+noncomputable def sol (k y₀ : ℝ → ℝ) (s : ℝ) : ℝ := iter k y₀ ⌈s⌉₊ s
+
+end Delay
+
+/-- The kernel `x / (x - 1)²` of the delay equations, frozen to the left of `3`. -/
+noncomputable def delayKer (x : ℝ) : ℝ := max x 3 / (max x 3 - 1) ^ 2
+
+/-- Initial values of `𝔚` on `[2, 3]` (constant to the left of `2`). -/
+noncomputable def initW (s : ℝ) : ℝ := 1 / (max s 2 - 1) - log (max s 2 - 1)
+
+/-- Iwaniec's `𝔐` [I71, §3, Definition]: `𝔐(s) = 2 + 1/(s - 1) - log (s - 1)` on `[2, 3]`
+(constant `3` to the left of `2`) and `𝔐'(s) = -s/(s - 1)² 𝔐(s - 1)` for `s > 3`. -/
+noncomputable def bigM : ℝ → ℝ := Delay.sol (fun x => -delayKer x) (fun s => 2 + initW s)
+
+end IwaniecLinearSieve

LeanPool/IwaniecLinearSieve/Imports.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2026 Lean Pool contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Pool contributors
+-/
+module  -- shake: keep-all --deprecated_module: ignore
+
+-- Generated project imports; run `lake exe mk_all`.
+public import LeanPool.IwaniecLinearSieve
+public import LeanPool.IwaniecLinearSieve.Basic
+public import LeanPool.IwaniecLinearSieve.Definitions
+public import LeanPool.IwaniecLinearSieve.Jacobsthal
+public import LeanPool.IwaniecLinearSieve.Jacobsthal.Reduction
+public import LeanPool.IwaniecLinearSieve.Jacobsthal.ShiftedSieve
+public import LeanPool.IwaniecLinearSieve.LinearSieve.Calculus
+public import LeanPool.IwaniecLinearSieve.LinearSieve.Corollaries
+public import LeanPool.IwaniecLinearSieve.LinearSieve.Crude
+public import LeanPool.IwaniecLinearSieve.LinearSieve.Defs
+public import LeanPool.IwaniecLinearSieve.LinearSieve.Depth
+public import LeanPool.IwaniecLinearSieve.LinearSieve.Estimate
+public import LeanPool.IwaniecLinearSieve.LinearSieve.LemmaEleven
+public import LeanPool.IwaniecLinearSieve.LinearSieve.LemmaSeven
+public import LeanPool.IwaniecLinearSieve.LinearSieve.TheoremFive
+public import LeanPool.IwaniecLinearSieve.LinearSieve.TheoremFiveAux
+public import LeanPool.IwaniecLinearSieve.LinearSieve.TheoremFiveCount
+public import LeanPool.IwaniecLinearSieve.LinearSieve.TheoremFour
+public import LeanPool.IwaniecLinearSieve.LinearSieve.TheoremFourAsymp
+public import LeanPool.IwaniecLinearSieve.LinearSieve.TheoremFourAux
+public import LeanPool.IwaniecLinearSieve.PrimeSums
+public import LeanPool.IwaniecLinearSieve.PrimeSums.Error
+public import LeanPool.IwaniecLinearSieve.PrimeSums.Lemma13
+public import LeanPool.IwaniecLinearSieve.PrimeSums.Mertens
+public import LeanPool.IwaniecLinearSieve.PrimeSums.NthPrime
+public import LeanPool.IwaniecLinearSieve.PrimeSums.Product
+public import LeanPool.IwaniecLinearSieve.PrimeSums.SummationByParts
+public import LeanPool.IwaniecLinearSieve.Rosser
+public import LeanPool.IwaniecLinearSieve.SieveFunctions
+public import LeanPool.IwaniecLinearSieve.SieveFunctions.Bounds
+public import LeanPool.IwaniecLinearSieve.SieveFunctions.Defs
+public import LeanPool.IwaniecLinearSieve.SieveFunctions.LemmaFive
+public import LeanPool.IwaniecLinearSieve.SieveFunctions.Series
+public import LeanPool.IwaniecLinearSieve.SieveMajorants.Defs
+public import LeanPool.IwaniecLinearSieve.SieveMajorants.Delay
+public import LeanPool.IwaniecLinearSieve.SieveMajorants.Lemmas
+public import LeanPool.IwaniecLinearSieve.SieveMajorants.Majorants
+public import LeanPool.IwaniecLinearSieve.SieveMajorants.Properties
+public import LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.Auxiliary
+public import LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.EulerMaclaurin
+public import LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.MediumPNT
+public import LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.MellinCalculus
+public import LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.Rectangle
+public import LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.ResidueCalcOnRectangles
+public import LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.StrongPNT
+public import LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.ZetaBounds
+public import LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.ZetaConj

LeanPool/IwaniecLinearSieve/Jacobsthal.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+
+module
+
+public import LeanPool.IwaniecLinearSieve.Jacobsthal.Reduction
+import LeanPool.IwaniecLinearSieve.PrimeSums.NthPrime
+import LeanPool.IwaniecLinearSieve.PrimeSums.Product
+
+/-!
+# Jacobsthal's problem ([I78])
+
+Iwaniec's application of the linear sieve: if `m` consecutive integers are each divisible by one
+of `r ≥ 2` given primes, then `m ≪ (r log r)²`. The shifted sieve ([I78, Lemma 1],
+`Jacobsthal/ShiftedSieve.lean`) transfers the Rosser weights for the first `r` primes to any `r`
+primes; `Jacobsthal/Reduction.lean` combines it with `linearSieveEstimate`.
+
+This port preserves the dependency closure of the corollary. The upstream repository also
+formalizes other results of [I78], which are outside this import's scope.
+
+The sieve definitions, statements and proofs were produced by AI agents under Jason Davies's
+supervision. The vendored strong PNT proofs come from PrimeNumberTheoremAnd and its contributors;
+their upstream revision is recorded in the project card and each vendor module.
+-/
+
+@[expose] public section
+
+namespace IwaniecLinearSieve
+
+/-- **Iwaniec's theorem** ([I78, Corollary]): if `m` consecutive integers are each divisible by
+one of `r ≥ 2` given primes, then `m ≪ (r log r)²`. -/
+theorem iwaniecBound :
+    ∃ C : ℝ, ∀ S : Finset ℕ, (∀ p ∈ S, p.Prime) → 2 ≤ S.card →
+      ∀ (x : ℤ) (m : ℕ), (∀ k < m, ∃ p ∈ S, (p : ℤ) ∣ x + k) →
+        (m : ℝ) ≤ C * ((S.card : ℝ) * Real.log S.card) ^ 2 :=
+  iwaniecBound_of_estimates linearSieveEstimate R_lower nth_prime_le
+
+end IwaniecLinearSieve