The actual sieve prime set and restoration of omitted Euler factors

noncomputable def NairTenenbaum.sievePrimeSet (Q : Polynomial ℤ) (n : ℕ) (z : ℝ) : Finset ℕ

Primes below the sieve cutoff with positive root count and coprime to the modulus.

Equations

• NairTenenbaum.sievePrimeSet Q n z = {p ∈ Finset.filter Nat.Prime (Finset.range (⌊z⌋₊ + 1)) | ¬p ∣ n ∧ NairTenenbaum.rootCount Q p ≠ 0}

noncomputable def NairTenenbaum.sieveModulus (Q : Polynomial ℤ) (n : ℕ) (z : ℝ) : ℕ

The squarefree product of the selected sieve primes.

Equations

• NairTenenbaum.sieveModulus Q n z = ∏ p ∈ NairTenenbaum.sievePrimeSet Q n z, p

theorem NairTenenbaum.sievePrimeSet_prime (Q : Polynomial ℤ) (n : ℕ) (z : ℝ) {p : ℕ} (hp : p ∈ sievePrimeSet Q n z) : Nat.Prime p

theorem NairTenenbaum.sieveModulus_squarefree (Q : Polynomial ℤ) (n : ℕ) (z : ℝ) : Squarefree (sieveModulus Q n z)

theorem NairTenenbaum.sieveModulus_primeFactors (Q : Polynomial ℤ) (n : ℕ) (z : ℝ) : (sieveModulus Q n z).primeFactors = sievePrimeSet Q n z

theorem NairTenenbaum.sieveModulus_coprime (Q : Polynomial ℤ) (n : ℕ) (z : ℝ) : (sieveModulus Q n z).Coprime n

theorem NairTenenbaum.sieveModulus_root_pos (Q : Polynomial ℤ) (n : ℕ) (z : ℝ) {p : ℕ} (hp : Nat.Prime p) (hd : p ∣ sieveModulus Q n z) : 0 < rootCount Q p

theorem NairTenenbaum.sieveModulus_prime_le (Q : Polynomial ℤ) (n : ℕ) {z : ℝ} (hz : 0 ≤ z) {p : ℕ} (hp : p ∈ (sieveModulus Q n z).primeFactors) : ↑p ≤ z

theorem NairTenenbaum.sievePrimeSet_euler_eq (Q : Polynomial ℤ) (n : ℕ) (z : ℝ) : ∏ p ∈ sievePrimeSet Q n z, (1 - ↑(rootCount Q p) / ↑p) = ∏ p ∈ Finset.filter Nat.Prime (Finset.range (⌊z⌋₊ + 1)) with ¬p ∣ n, (1 - ↑(rootCount Q p) / ↑p)

theorem NairTenenbaum.sievePrimeSet_euler_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {g n : ℕ} (hg : Q.natDegree ≤ g) (hn : n ≠ 0) (z : ℝ) : ∏ p ∈ sievePrimeSet Q n z, (1 - ↑(rootCount Q p) / ↑p) ≤ omittedEulerBound g * sieveProduct Q z * totientTwist g n

Restoring the omitted primes gives precisely the totient correction needed by the smooth-weight comparison.

theorem NairTenenbaum.exists_restored_conditional_sieve_bound {g : ℕ} (hg : 0 < g) {η : ℝ} (hη : 0 < η) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (Q : Polynomial ℤ), NoFixedPrimeDivisor Q → Q.natDegree ≤ g → ∀ (r : ℕ) (R : Fin r → Polynomial ℤ) (m : Tuple r), (Pairwise fun (i j : Fin r) => (↑(m i)).Coprime ↑(m j)) → ∀ (a b : ℤ) (z : ℝ), a ≤ b → 2 ≤ z → 16 ≤ Real.log z → ↑(conditionalPolynomialSiftedCount Q (sieveModulus Q (mass m) z) R m a b) ≤ K * ((↑b - ↑a) * sieveProduct Q z * totientTwist g (mass m) * ∏ i : Fin r, ↑(rootCount (R i) ↑(m i)) / ↑↑(m i) + (∏ i : Fin r, ↑(rootCount (R i) ↑(m i))) * z ^ (4 * ↑g * (1 + η)))

The conditional sieve with the full Euler product restored. Its only modulus-dependent correction is the standard totient twist.