Notation for [I71, §4]

L = log y, ξ(y) = log y / (log log 3y)^{11/5}, δ(s, y) = (1 + s² log⁵ s / log² y)^{5s}. The main-term majorants are f (lower sieve) and F + (3 - s)⁺ (upper sieve, which also contains the depth-one deficit); the error majorants are 𝔣 and 𝔉.

noncomputable def IwaniecLinearSieve.xi (y : ℝ) : ℝ

Iwaniec's ξ = log y / (log log 3y)^{11/5}.

Equations

• IwaniecLinearSieve.xi y = Real.log y / Real.log (Real.log (3 * y)) ^ (11 / 5)

noncomputable def IwaniecLinearSieve.delta (s y : ℝ) : ℝ

Iwaniec's compensation factor (1 + s² log⁵ s / log² y)^{5s}.

Equations

• IwaniecLinearSieve.delta s y = (1 + s ^ 2 * Real.log s ^ 5 / Real.log y ^ 2) ^ (5 * s)

noncomputable def IwaniecLinearSieve.mainMaj : Bool → ℝ → ℝ

Main-term majorants: f for the lower sieve, F + (3 - s)⁺ for the upper sieve.

Equations

• IwaniecLinearSieve.mainMaj true x✝ = IwaniecLinearSieve.fSieve x✝
• IwaniecLinearSieve.mainMaj false x✝ = IwaniecLinearSieve.FSieve x✝ + max (3 - x✝) 0

noncomputable def IwaniecLinearSieve.errMaj : Bool → ℝ → ℝ

Error majorants G: 𝔣 for the lower sieve, 𝔉 for the upper sieve.

Equations

• IwaniecLinearSieve.errMaj true = IwaniecLinearSieve.majf
• IwaniecLinearSieve.errMaj false = IwaniecLinearSieve.majF

def IwaniecLinearSieve.sMin : Bool → ℝ

The smallest sifting parameter s: 2 for the lower sieve, 1 for the upper sieve.

Equations

• IwaniecLinearSieve.sMin true = 2
• IwaniecLinearSieve.sMin false = 1