Absorbing the prime-argument sieve remainder

The additional logarithm costs an arbitrarily small power in the sieve level. The threshold is uniform in the constant term of the original polynomial.

theorem NairTenenbaum.exists_sieveProduct_inv_mul_log_le_rpow (g : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ (Q : Polynomial ℤ), NoFixedPrimeDivisor Q → Q.natDegree ≤ g → ∀ (z : ℝ), 2 ≤ z → (sieveProduct Q z)⁻¹ * Real.log z ≤ B * z ^ δ

noncomputable def NairTenenbaum.primeArgumentConditionalMainTerm {r : ℕ} (Q : Polynomial ℤ) (g : ℕ) (R : Fin r → Polynomial ℤ) (m : Tuple r) (a b : ℤ) (z : ℝ) : ℝ

The conditional sieve main term with the prime-argument corrections.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.exists_primeArgument_conditional_sieve_level_bound (g : ℕ) {η δ : ℝ} (hη : 0 < η) (hδ : 0 < δ) : ∃ (K : ℝ) (B : ℝ), 1 ≤ K ∧ 1 ≤ B ∧ ∀ (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 → B * ↑(mass m) * z ^ (4 * (↑g + 1) * (1 + η) + δ) ≤ ↑b - ↑a → ↑(conditionalPolynomialSiftedCount (Q * Polynomial.X) (primeArgumentSieveModulus Q g (mass m) z) R m a b) ≤ K * primeArgumentConditionalMainTerm Q g R m a b z