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⌉₊.

noncomputable def IwaniecLinearSieve.primorialLT (z : ℝ) : ℕ

P(z) = ∏_{p < z} p.

Equations

• IwaniecLinearSieve.primorialLT z = ∏ p ∈ IwaniecLinearSieve.primesLT z, p

noncomputable def IwaniecLinearSieve.R (z : ℝ) : ℝ

Iwaniec's R(z) = ∏_{p < z} (1 - 1/p) (his R_k with k = 1).

Equations

• IwaniecLinearSieve.R z = ∏ p ∈ IwaniecLinearSieve.primesLT z, (1 - (↑p)⁻¹)

theorem IwaniecLinearSieve.mem_primesLT {z : ℝ} {p : ℕ} : p ∈ primesLT z ↔ Nat.Prime p ∧ ↑p < z

theorem IwaniecLinearSieve.R_nonneg (z : ℝ) : 0 ≤ R z

theorem IwaniecLinearSieve.R_pos (z : ℝ) : 0 < R z