The Selberg upper bound for polynomial values in intervals

noncomputable def NairTenenbaum.rootDensity (Q : Polynomial ℤ) : ArithmeticFunction ℝ

Polynomial congruence density as a multiplicative arithmetic function.

Equations

• NairTenenbaum.rootDensity Q = { toFun := fun (d : ℕ) => ↑(NairTenenbaum.rootCount Q d) / ↑d, map_zero' := ⋯ }

theorem NairTenenbaum.rootDensity_apply (Q : Polynomial ℤ) (d : ℕ) : (rootDensity Q) d = ↑(rootCount Q d) / ↑d

theorem NairTenenbaum.rootDensity_multiplicative (Q : Polynomial ℤ) : (rootDensity Q).IsMultiplicative

theorem NairTenenbaum.rootCount_squarefree {Q : Polynomial ℤ} {n : ℕ} (hn : Squarefree n) : rootCount Q n = ∏ p ∈ n.primeFactors, rootCount Q p

theorem NairTenenbaum.rootCount_squarefree_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {g : ℝ} (hg : ↑Q.natDegree ≤ g) {n : ℕ} (hn : Squarefree n) : ↑(rootCount Q n) ≤ g ^ n.primeFactors.card

theorem NairTenenbaum.sum_fiber_card_filter {ι : Type u_1} (T : Finset ι) (f : ι → ℕ) (pred : ℕ → Prop) [DecidablePred pred] : (∑ d ∈ Finset.image f T, if pred d then ↑{n ∈ T | f n = d}.card else 0) = ↑{n ∈ T | pred (f n)}.card

Counting fibers transfers a finite set to natural-valued sieve support, without assuming that the value map is injective.

noncomputable def NairTenenbaum.polynomialBoundingSieve (Q : Polynomial ℤ) (hQ : NoFixedPrimeDivisor Q) (P : ℕ) (hP : Squarefree P) (hroot : ∀ (p : ℕ), Nat.Prime p → p ∣ P → 0 < rootCount Q p) (a b : ℤ) : BoundingSieve

The Selberg bounding sieve attached to polynomial values on an interval.

Equations

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

theorem NairTenenbaum.polynomialBoundingSieve_multSum (Q : Polynomial ℤ) (hQ : NoFixedPrimeDivisor Q) (P : ℕ) (hP : Squarefree P) (hroot : ∀ (p : ℕ), Nat.Prime p → p ∣ P → 0 < rootCount Q p) (a b : ℤ) (d : ℕ) : BoundingSieve.multSum d = ↑(polynomialCongruenceCount Q d a b)

theorem NairTenenbaum.polynomialBoundingSieve_rem_le (Q : Polynomial ℤ) (hQ : NoFixedPrimeDivisor Q) (P : ℕ) (hP : Squarefree P) (hroot : ∀ (p : ℕ), Nat.Prime p → p ∣ P → 0 < rootCount Q p) (a b : ℤ) (hab : a ≤ b) {d : ℕ} (hd : d ∣ P) : |BoundingSieve.rem d| ≤ ↑(rootCount Q d)

noncomputable def NairTenenbaum.polynomialSiftedCount (Q : Polynomial ℤ) (P : ℕ) (a b : ℤ) : ℕ

The number of polynomial values coprime to the sieve modulus.

Equations

• NairTenenbaum.polynomialSiftedCount Q P a b = {n ∈ Finset.Ioc a b | P.Coprime (Polynomial.eval n Q).natAbs}.card

theorem NairTenenbaum.polynomialBoundingSieve_siftedSum (Q : Polynomial ℤ) (hQ : NoFixedPrimeDivisor Q) (P : ℕ) (hP : Squarefree P) (hroot : ∀ (p : ℕ), Nat.Prime p → p ∣ P → 0 < rootCount Q p) (a b : ℤ) : BoundingSieve.siftedSum = ↑(polynomialSiftedCount Q P a b)

theorem NairTenenbaum.exists_polynomial_sieve_bound {g η : ℝ} (hg : 1 ≤ g) (hη : 0 < η) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (Q : Polynomial ℤ), NoFixedPrimeDivisor Q → ↑Q.natDegree ≤ g → ∀ (P : ℕ), Squarefree P → (∀ (p : ℕ), Nat.Prime p → p ∣ P → 0 < rootCount Q p) → ∀ (a b : ℤ) (z : ℝ), a ≤ b → 2 ≤ z → 16 ≤ Real.log z → (∀ p ∈ P.primeFactors, ↑p ≤ z) → ↑(polynomialSiftedCount Q P a b) ≤ 4 * (↑b - ↑a) * ∏ p ∈ P.primeFactors, (1 - ↑(rootCount Q p) / ↑p) + K * z ^ (4 * g * (1 + η))

A polynomial sieve bound with constants independent of the coefficients, the interval, and the selected primes. Root-free primes can simply be omitted.