The conditional sieve for prime arguments

We sieve Q(t) * t, omitting primes dividing the congruence modulus or (g+1)!. The latter omission removes every possible fixed prime of the enlarged polynomial, at a cost depending only on the original degree bound.

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

The sieve modulus for the total polynomial times X, omitting obstructed primes.

Equations

• NairTenenbaum.primeArgumentSieveModulus Q g n z = NairTenenbaum.sieveModulus (Q * Polynomial.X) (n * (g + 1).factorial) z

theorem NairTenenbaum.primeArgumentSieveModulus_squarefree (Q : Polynomial ℤ) (g n : ℕ) (z : ℝ) : Squarefree (primeArgumentSieveModulus Q g n z)

theorem NairTenenbaum.primeArgumentSieveModulus_coprime (Q : Polynomial ℤ) (g n : ℕ) (z : ℝ) : (primeArgumentSieveModulus Q g n z).Coprime n

theorem NairTenenbaum.primeArgumentSieveModulus_large_prime (Q : Polynomial ℤ) (g n : ℕ) (z : ℝ) {p : ℕ} (hp : Nat.Prime p) (hd : p ∣ primeArgumentSieveModulus Q g n z) : g + 1 < p

theorem NairTenenbaum.primeArgumentSieveModulus_root_lt {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {g : ℕ} (hdeg : Q.natDegree ≤ g) (n : ℕ) (z : ℝ) {p : ℕ} (hp : Nat.Prime p) (hd : p ∣ primeArgumentSieveModulus Q g n z) : rootCount (Q * Polynomial.X) p < p

The small-prime exclusion makes the enlarged polynomial admissible at every selected prime; it requires no global admissibility of Q * X.

theorem NairTenenbaum.primeArgumentSieveModulus_coprime_prime (Q : Polynomial ℤ) (g n : ℕ) {z : ℝ} (hz : 0 ≤ z) {t : ℕ} (ht : Nat.Prime t) (hzt : z < ↑t) : (primeArgumentSieveModulus Q g n z).Coprime t

Every prime argument above the sieve cutoff survives the sieve of X.

theorem NairTenenbaum.primeArgumentSieveModulus_coprime_value (Q : Polynomial ℤ) (g n : ℕ) {z : ℝ} (hz : 0 ≤ z) (t : ℤ) (hsift : (sieveModulus Q n z).Coprime (Polynomial.eval t Q).natAbs) : (primeArgumentSieveModulus Q g n z).Coprime (Polynomial.eval t Q).natAbs

Passing from the original sieve to the enlarged sieve removes constraints on Q(t) only. A prime with zero root count cannot divide a polynomial value.

theorem NairTenenbaum.primeArgumentSieveModulus_coprime_mul_X (Q : Polynomial ℤ) (g n : ℕ) {z : ℝ} (hz : 0 ≤ z) (t : ℤ) (ht : Nat.Prime t.natAbs) (hzt : z < ↑t.natAbs) (hsift : (sieveModulus Q n z).Coprime (Polynomial.eval t Q).natAbs) : (primeArgumentSieveModulus Q g n z).Coprime (Polynomial.eval t (Q * Polynomial.X)).natAbs

The original roughness condition and primality together imply the enlarged sieve condition used in the conditional estimate.

noncomputable def NairTenenbaum.primeArgumentEulerConstant (g : ℕ) : ℝ

The degree-dependent constant in the prime-argument Euler-product comparison.

Equations

• NairTenenbaum.primeArgumentEulerConstant g = NairTenenbaum.omittedEulerBound g * NairTenenbaum.totientTwist (g + 1) (g + 1).factorial

theorem NairTenenbaum.primeArgumentEulerConstant_pos (g : ℕ) : 0 < primeArgumentEulerConstant g

theorem NairTenenbaum.primeArgumentSieveModulus_euler_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hzero : Polynomial.eval 0 Q ≠ 0) {g n : ℕ} (hdeg : Q.natDegree ≤ g) (hn : n ≠ 0) {z : ℝ} (hz : 1 < z) : ∏ p ∈ (primeArgumentSieveModulus Q g n z).primeFactors, (1 - ↑(rootCount (Q * Polynomial.X) p) / ↑p) ≤ primeArgumentEulerConstant g * sieveProduct Q z * totientTwist 1 (Polynomial.eval 0 Q).natAbs * totientTwist (g + 1) n / Real.log z

The conditional prime-argument sieve retains the original polynomial's Euler product and costs one additional totient twist on the prefix modulus.

theorem NairTenenbaum.exists_primeArgument_conditional_sieve_bound (g : ℕ) {η : ℝ} (hη : 0 < η) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (Q : Polynomial ℤ), NoFixedPrimeDivisor Q → Polynomial.eval 0 Q ≠ 0 → 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 * Polynomial.X) (primeArgumentSieveModulus Q g (mass m) z) R m a b) ≤ K * ((↑b - ↑a) * sieveProduct Q z * totientTwist 1 (Polynomial.eval 0 Q).natAbs * totientTwist (g + 1) (mass m) / Real.log z * ∏ i : Fin r, ↑(rootCount (R i) ↑(m i)) / ↑↑(m i) + (∏ i : Fin r, ↑(rootCount (R i) ↑(m i))) * z ^ (4 * (↑g + 1) * (1 + η)))

The restored conditional estimate for sieving prime arguments. The constant depends only on the original degree bound and the sieve slack. Congruence densities, the totient correction at Q(0), and the logarithmic saving all remain explicit.