Congruence counts in intervals

The elementary distribution estimate needed as input to the polynomial sieve: |#{a < n ≤ b : q ∣ Q(n)} - (b-a)ρ_Q(q)/q| ≤ ρ_Q(q). No primality or squarefreeness assumption on the positive modulus is needed.

theorem NairTenenbaum.residue_count_error (a b v : ℤ) (hab : a ≤ b) {q : ℕ} (hq : 0 < q) : |↑{n ∈ Finset.Ioc a b | n ≡ v [ZMOD ↑q]}.card - (↑b - ↑a) / ↑q| ≤ 1

The count of one residue class differs from interval length divided by its modulus by at most one. Integer endpoints may be negative.

def NairTenenbaum.residueRootSet (Q : Polynomial ℤ) (q : ℕ) [NeZero q] : Finset (ZMod q)

The roots as a finite set, for a positive modulus.

Equations

• NairTenenbaum.residueRootSet Q q = {a : ZMod q | Polynomial.eval₂ (Int.castRingHom (ZMod q)) a Q = 0}

theorem NairTenenbaum.residueRootSet_card (Q : Polynomial ℤ) (q : ℕ) [NeZero q] : (residueRootSet Q q).card = rootCount Q q

theorem NairTenenbaum.cast_mem_residueRootSet (Q : Polynomial ℤ) (q : ℕ) [NeZero q] (n : ℤ) : ↑n ∈ residueRootSet Q q ↔ ↑q ∣ Polynomial.eval n Q

noncomputable def NairTenenbaum.polynomialCongruenceCount (Q : Polynomial ℤ) (q : ℕ) (a b : ℤ) : ℕ

Polynomial congruences in (a,b].

Equations

• NairTenenbaum.polynomialCongruenceCount Q q a b = {n ∈ Finset.Ioc a b | ↑q ∣ Polynomial.eval n Q}.card

theorem NairTenenbaum.polynomialCongruenceCount_eq_sum (Q : Polynomial ℤ) (q : ℕ) [NeZero q] (a b : ℤ) : polynomialCongruenceCount Q q a b = ∑ r ∈ residueRootSet Q q, {n ∈ Finset.Ioc a b | n ≡ ↑r.val [ZMOD ↑q]}.card

theorem NairTenenbaum.polynomialCongruenceCount_error (Q : Polynomial ℤ) {q : ℕ} (hq : 0 < q) (a b : ℤ) (hab : a ≤ b) : |↑(polynomialCongruenceCount Q q a b) - (↑b - ↑a) * ↑(rootCount Q q) / ↑q| ≤ ↑(rootCount Q q)

The interval distribution estimate for polynomial congruences.