Absorbing the conditional sieve remainder at an explicit level

theorem NairTenenbaum.mass_mul_root_density {r : ℕ} (R : Fin r → Polynomial ℤ) (m : Tuple r) : ↑(mass m) * ∏ i : Fin r, ↑(rootCount (R i) ↑(m i)) / ↑↑(m i) = ∏ i : Fin r, ↑(rootCount (R i) ↑(m i))

theorem NairTenenbaum.absorb_sieve_remainder {K B M D S T L z A δ count : ℝ} (hK : 0 ≤ K) (hM : 0 ≤ M) (hD : 0 ≤ D) (hS : 0 < S) (hT : 1 ≤ T) (hL : 0 ≤ L) (hz : 0 < z) (hinv : S⁻¹ ≤ B * z ^ δ) (hlevel : B * M * z ^ (A + δ) ≤ L) (hcount : count ≤ K * (L * S * T * D + M * D * z ^ A)) : count ≤ 2 * K * (L * S * T * D)

A power bound for the reciprocal sieve density absorbs the remainder at the given level.

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

The conditional sieve main term with its congruence density and totient correction.

Equations

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

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

Explicit cutoff growth is sufficient to absorb the entire conditional sieve remainder, uniformly in the conditioning polynomials and moduli.