Conditional sieves using admissibility only at the selected primes

Adjoining X to a polynomial can introduce fixed prime divisors. The Selberg bound needs a strict root-density bound only at primes actually being sieved. This version records that local hypothesis explicitly and allows those finitely many obstructions to be omitted.

noncomputable def NairTenenbaum.polynomialCongruenceSet {r : ℕ} (R : Fin r → Polynomial ℤ) (m : Tuple r) (a b : ℤ) : Finset ℤ

The integers in an interval satisfying the coordinate polynomial divisibility conditions.

Equations

• NairTenenbaum.polynomialCongruenceSet R m a b = {n ∈ Finset.Ioc a b | ∀ (i : Fin r), ↑↑(m i) ∣ Polynomial.eval n (R i)}

theorem NairTenenbaum.mixedCongruenceCount_error {r : ℕ} (Q : Polynomial ℤ) (R : Fin r → Polynomial ℤ) {d : ℕ} (hd : 0 < d) (m : Tuple r) (hpair : Pairwise fun (i j : Fin r) => (↑(m i)).Coprime ↑(m j)) (hcross : ∀ (i : Fin r), d.Coprime ↑(m i)) (a b : ℤ) (hab : a ≤ b) : |↑(mixedCongruenceCount Q R d m a b) - ↑(rootCount Q d) / ↑d * ((↑b - ↑a) * ∏ i : Fin r, ↑(rootCount (R i) ↑(m i)) / ↑↑(m i))| ≤ ↑(rootCount Q d) * ∏ i : Fin r, ↑(rootCount (R i) ↑(m i))

noncomputable def NairTenenbaum.conditionalPolynomialSiftedCount {r : ℕ} (Q : Polynomial ℤ) (P : ℕ) (R : Fin r → Polynomial ℤ) (m : Tuple r) (a b : ℤ) : ℕ

The congruence count after imposing coprimality with the sieve modulus.

Equations

• NairTenenbaum.conditionalPolynomialSiftedCount Q P R m a b = {n ∈ NairTenenbaum.polynomialCongruenceSet R m a b | P.Coprime (Polynomial.eval n Q).natAbs}.card

noncomputable def NairTenenbaum.localConditionalPolynomialSieve {r : ℕ} (Q : Polynomial ℤ) (P : ℕ) (hP : Squarefree P) (hQ : ∀ (p : ℕ), Nat.Prime p → p ∣ P → rootCount Q p < p) (hroot : ∀ (p : ℕ), Nat.Prime p → p ∣ P → 0 < rootCount Q p) (R : Fin r → Polynomial ℤ) (m : Tuple r) (a b : ℤ) : BoundingSieve

A conditional Selberg sieve requiring strict root-density bounds only at selected primes.

Equations

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

theorem NairTenenbaum.localConditionalPolynomialSieve_multSum {r : ℕ} (Q : Polynomial ℤ) (P : ℕ) (hP : Squarefree P) (hQ : ∀ (p : ℕ), Nat.Prime p → p ∣ P → rootCount Q p < p) (hroot : ∀ (p : ℕ), Nat.Prime p → p ∣ P → 0 < rootCount Q p) (R : Fin r → Polynomial ℤ) (m : Tuple r) (a b : ℤ) (d : ℕ) : BoundingSieve.multSum d = ↑(mixedCongruenceCount Q R d m a b)

theorem NairTenenbaum.localConditionalPolynomialSieve_rem_le {r : ℕ} (Q : Polynomial ℤ) (P : ℕ) (hP : Squarefree P) (hQ : ∀ (p : ℕ), Nat.Prime p → p ∣ P → rootCount Q p < p) (hroot : ∀ (p : ℕ), Nat.Prime p → p ∣ P → 0 < rootCount Q p) (R : Fin r → Polynomial ℤ) (m : Tuple r) (hpair : Pairwise fun (i j : Fin r) => (↑(m i)).Coprime ↑(m j)) (hPm : P.Coprime (mass m)) (a b : ℤ) (hab : a ≤ b) {d : ℕ} (hd : d ∣ P) : |BoundingSieve.rem d| ≤ ↑(rootCount Q d) * ∏ i : Fin r, ↑(rootCount (R i) ↑(m i))

theorem NairTenenbaum.localConditionalPolynomialSieve_siftedSum {r : ℕ} (Q : Polynomial ℤ) (P : ℕ) (hP : Squarefree P) (hQ : ∀ (p : ℕ), Nat.Prime p → p ∣ P → rootCount Q p < p) (hroot : ∀ (p : ℕ), Nat.Prime p → p ∣ P → 0 < rootCount Q p) (R : Fin r → Polynomial ℤ) (m : Tuple r) (a b : ℤ) : BoundingSieve.siftedSum = ↑(conditionalPolynomialSiftedCount Q P R m a b)

theorem NairTenenbaum.exists_local_conditional_polynomial_sieve_bound {g η : ℝ} (hg : 1 ≤ g) (hη : 0 < η) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (Q : Polynomial ℤ) (P : ℕ), Squarefree P → (∀ (p : ℕ), Nat.Prime p → p ∣ P → rootCount Q p < p) → (∀ (p : ℕ), Nat.Prime p → p ∣ P → ↑(rootCount Q p) ≤ g) → (∀ (p : ℕ), Nat.Prime p → p ∣ P → 0 < rootCount Q p) → ∀ (r : ℕ) (R : Fin r → Polynomial ℤ) (m : Tuple r), (Pairwise fun (i j : Fin r) => (↑(m i)).Coprime ↑(m j)) → P.Coprime (mass m) → ∀ (a b : ℤ) (z : ℝ), a ≤ b → 2 ≤ z → 16 ≤ Real.log z → (∀ p ∈ P.primeFactors, ↑p ≤ z) → ↑(conditionalPolynomialSiftedCount Q P R m a b) ≤ (4 * (↑b - ↑a) * ∏ i : Fin r, ↑(rootCount (R i) ↑(m i)) / ↑↑(m i)) * ∏ p ∈ P.primeFactors, (1 - ↑(rootCount Q p) / ↑p) + (K * ∏ i : Fin r, ↑(rootCount (R i) ↑(m i))) * z ^ (4 * g * (1 + η))

The congruence density remains in the main term; its numerator controls the error. The constant is uniform in the congruence polynomials and moduli.