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.

Sifted sets ([I71, §1])

noncomputable def IwaniecLinearSieve.primesLT (z : ℝ) : Finset ℕ

The primes p < z.

Equations

• IwaniecLinearSieve.primesLT z = ⌈z⌉₊.primesBelow

noncomputable def IwaniecLinearSieve.primesLTk (k : ℕ) (z : ℝ) : Finset ℕ

The primes p < z with p ∤ k.

Equations

• IwaniecLinearSieve.primesLTk k z = {p ∈ IwaniecLinearSieve.primesLT z | ¬p ∣ k}

noncomputable def IwaniecLinearSieve.Rk (k : ℕ) (z : ℝ) : ℝ

Iwaniec's R_k(z) = ∏_{p < z, p ∤ k} (1 - 1/p).

Equations

• IwaniecLinearSieve.Rk k z = ∏ p ∈ IwaniecLinearSieve.primesLTk k z, (1 - (↑p)⁻¹)

noncomputable def IwaniecLinearSieve.siftedCount (k : ℕ) (M : Multiset ℤ) (z : ℝ) : ℕ

Iwaniec's A_k(M; z): the number of terms of M not divisible by any prime p < z with p ∤ k.

Equations

• IwaniecLinearSieve.siftedCount k M z = Multiset.countP (fun (a : ℤ) => ∀ p ∈ IwaniecLinearSieve.primesLTk k z, ¬↑p ∣ a) M

def IwaniecLinearSieve.multiplesCount (M : Multiset ℤ) (d : ℕ) : ℕ

Iwaniec's |M_d|: the number of terms of M divisible by d.

Equations

• IwaniecLinearSieve.multiplesCount M d = Multiset.countP (fun (a : ℤ) => ↑d ∣ a) M

The sieve functions f and F ([I71, §3, (3.1)–(3.7)])

noncomputable def IwaniecLinearSieve.gTwoFormula (s : ℝ) : ℝ

The formula 3 log (3 / (s - 1)) + s - 4 for g₂ on [2, 4].

Equations

• IwaniecLinearSieve.gTwoFormula s = 3 * Real.log (3 / (s - 1)) + s - 4

noncomputable def IwaniecLinearSieve.gLower (i : ℕ) : ℝ

Left end of the domain of g i in [I71]: 2 for even i, 3 for odd i.

Equations

• IwaniecLinearSieve.gLower i = if Even i then 2 else 3

noncomputable def IwaniecLinearSieve.shiftKernel (h : ℝ → ℝ) (t : ℝ) : ℝ

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.

Equations

• IwaniecLinearSieve.shiftKernel h t = h (t - 1) / max (t - 1) 1

noncomputable def IwaniecLinearSieve.g : ℕ → ℝ → ℝ

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.

Equations

• IwaniecLinearSieve.g 0 x✝ = 0
• IwaniecLinearSieve.g 1 x✝ = 0
• IwaniecLinearSieve.g 2 x✝ = IwaniecLinearSieve.gTwoFormula (max 2 (min x✝ 4))
• IwaniecLinearSieve.g n.succ.succ.succ x✝ = ∫ (t : ℝ) in max x✝ (IwaniecLinearSieve.gLower (n + 3))..↑n + 5, IwaniecLinearSieve.shiftKernel (IwaniecLinearSieve.g (n + 2)) t

noncomputable def IwaniecLinearSieve.fSieve (s : ℝ) : ℝ

Iwaniec's f(s) = Σ_{i ≥ 1} g_{2i}(s) [I71, (3.6)]; constant (= f(2) = 2) for s ≤ 2.

Equations

• IwaniecLinearSieve.fSieve s = ∑' (n : ℕ), IwaniecLinearSieve.g (2 * n + 2) s

noncomputable def IwaniecLinearSieve.FSieve (s : ℝ) : ℝ

Iwaniec's F(s) = Σ_{i ≥ 1} g_{2i+1}(s) [I71, (3.7)]; constant (= F(3)) for s ≤ 3.

Equations

• IwaniecLinearSieve.FSieve s = ∑' (n : ℕ), IwaniecLinearSieve.g (2 * n + 3) s

The function 𝔐 ([I71, §3, Definition])

noncomputable def IwaniecLinearSieve.Delay.step (k y₀ y : ℝ → ℝ) (s : ℝ) : ℝ

One Picard-type step: y₀ up to 3, then integrate k x * y (x - 1) from 3.

Equations

• IwaniecLinearSieve.Delay.step k y₀ y s = y₀ (min s 3) + ∫ (x : ℝ) in 3..max s 3, k x * y (x - 1)

noncomputable def IwaniecLinearSieve.Delay.iter (k y₀ : ℝ → ℝ) : ℕ → ℝ → ℝ

The iterates of step; the n-th one is correct on (-∞, n + 3].

Equations

• IwaniecLinearSieve.Delay.iter k y₀ 0 = y₀
• IwaniecLinearSieve.Delay.iter k y₀ n.succ = IwaniecLinearSieve.Delay.step k y₀ (IwaniecLinearSieve.Delay.iter k y₀ n)

noncomputable def IwaniecLinearSieve.Delay.sol (k y₀ : ℝ → ℝ) (s : ℝ) : ℝ

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.

Equations

• IwaniecLinearSieve.Delay.sol k y₀ s = IwaniecLinearSieve.Delay.iter k y₀ ⌈s⌉₊ s

noncomputable def IwaniecLinearSieve.delayKer (x : ℝ) : ℝ

The kernel x / (x - 1)² of the delay equations, frozen to the left of 3.

Equations

• IwaniecLinearSieve.delayKer x = max x 3 / (max x 3 - 1) ^ 2

noncomputable def IwaniecLinearSieve.initW (s : ℝ) : ℝ

Initial values of 𝔚 on [2, 3] (constant to the left of 2).

Equations

• IwaniecLinearSieve.initW s = 1 / (max s 2 - 1) - Real.log (max s 2 - 1)

noncomputable def IwaniecLinearSieve.bigM : ℝ → ℝ

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.

Equations

• IwaniecLinearSieve.bigM = IwaniecLinearSieve.Delay.sol (fun (x : ℝ) => -IwaniecLinearSieve.delayKer x) fun (s : ℝ) => 2 + IwaniecLinearSieve.initW s