Polynomial root counts, equation (10)

The roots are residue classes, so multiplicities of polynomial roots are not counted. The Chinese remainder theorem gives multiplicativity for all coprime positive moduli.

@[reducible, inline]

abbrev NairTenenbaum.ResidueRoots (Q : Polynomial ℤ) (n : ℕ) : Type

Roots of an integral polynomial in the specified residue ring.

Equations

• NairTenenbaum.ResidueRoots Q n = { a : ZMod n // Polynomial.eval₂ (Int.castRingHom (ZMod n)) a Q = 0 }

noncomputable def NairTenenbaum.rootCount (Q : Polynomial ℤ) (n : ℕ) : ℕ

ρ_Q(n), the number of roots modulo n. Only positive moduli are used.

Equations

• NairTenenbaum.rootCount Q n = Nat.card (NairTenenbaum.ResidueRoots Q n)

theorem NairTenenbaum.eval₂_int_cast_natural {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (Q : Polynomial ℤ) (a : R) : f (Polynomial.eval₂ (Int.castRingHom R) a Q) = Polynomial.eval₂ (Int.castRingHom S) (f a) Q

noncomputable def NairTenenbaum.rootsCRT (Q : Polynomial ℤ) {m n : ℕ} (h : m.Coprime n) : ResidueRoots Q (m * n) ≃ ResidueRoots Q m × ResidueRoots Q n

The CRT equivalence restricted to the zero loci.

Equations

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

theorem NairTenenbaum.rootCount_mul (Q : Polynomial ℤ) {m n : ℕ} (h : m.Coprime n) : rootCount Q (m * n) = rootCount Q m * rootCount Q n

@[simp]

theorem NairTenenbaum.rootCount_one (Q : Polynomial ℤ) : rootCount Q 1 = 1

theorem NairTenenbaum.rootCount_le (Q : Polynomial ℤ) {n : ℕ} (hn : n ≠ 0) : rootCount Q n ≤ n

theorem NairTenenbaum.rootCount_le_of_dvd {Q T : Polynomial ℤ} (hQT : Q ∣ T) {n : ℕ} (hn : n ≠ 0) : rootCount Q n ≤ rootCount T n

Dividing a polynomial can only remove residue roots.

theorem NairTenenbaum.rootCount_C_mul_unit (Q : Polynomial ℤ) {u : ℤ} (hu : IsUnit u) (n : ℕ) : rootCount (Polynomial.C u * Q) n = rootCount Q n

Multiplication by an integral unit does not change the residue roots.

@[simp]

theorem NairTenenbaum.rootCount_X (n : ℕ) : rootCount Polynomial.X n = 1

def NairTenenbaum.NoFixedPrimeDivisor (Q : Polynomial ℤ) : Prop

The paper's admissibility condition on polynomials.

Equations

• NairTenenbaum.NoFixedPrimeDivisor Q = ∀ (p : ℕ), Nat.Prime p → NairTenenbaum.rootCount Q p < p

theorem NairTenenbaum.NoFixedPrimeDivisor.of_dvd {Q T : Polynomial ℤ} (hT : NoFixedPrimeDivisor T) (hQT : Q ∣ T) : NoFixedPrimeDivisor Q

theorem NairTenenbaum.noFixedPrimeDivisor_X : NoFixedPrimeDivisor Polynomial.X

theorem NairTenenbaum.rootCount_prod_pow_prime {ι : Type u_1} [Fintype ι] (R : ι → Polynomial ℤ) (γ : ι → ℕ) (hγ : ∀ (i : ι), 0 < γ i) {p : ℕ} (hp : Nat.Prime p) : rootCount (∏ i : ι, R i ^ γ i) p = rootCount (∏ i : ι, R i) p

Removing positive powers from a product does not change its roots modulo a prime.

theorem NairTenenbaum.rootCount_X_add_C (b : ℤ) (n : ℕ) : rootCount (Polynomial.X + Polynomial.C b) n = 1

A translate of X has exactly one root for every positive modulus.

theorem NairTenenbaum.noFixedPrimeDivisor_X_add_C (b : ℤ) : NoFixedPrimeDivisor (Polynomial.X + Polynomial.C b)

theorem NairTenenbaum.rootCount_eq_card_filter (Q : Polynomial ℤ) (n : ℕ) [NeZero n] : rootCount Q n = {a : ZMod n | Polynomial.eval₂ (Int.castRingHom (ZMod n)) a Q = 0}.card

theorem NairTenenbaum.NoFixedPrimeDivisor.map_ne_zero {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {p : ℕ} (hp : Nat.Prime p) : Polynomial.map (Int.castRingHom (ZMod p)) Q ≠ 0

A polynomial with no fixed prime divisor cannot become the zero polynomial after reduction modulo a prime.

theorem NairTenenbaum.rootCount_le_degree {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {p : ℕ} (hp : Nat.Prime p) : rootCount Q p ≤ Q.natDegree

The standard prime-modulus root bound used in the sieve.

noncomputable def NairTenenbaum.sieveProduct (Q : Polynomial ℤ) (x : ℝ) : ℝ

The local sieve factor in Theorem 1.

Equations

• NairTenenbaum.sieveProduct Q x = ∏ p ∈ Finset.range (⌊x⌋₊ + 1) with Nat.Prime p, (1 - ↑(NairTenenbaum.rootCount Q p) / ↑p)

theorem NairTenenbaum.sieveProduct_pos {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (x : ℝ) : 0 < sieveProduct Q x

theorem NairTenenbaum.primeSet_product_squarefree (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) : Squarefree (∏ p ∈ S, p)

A finite product of distinct primes is squarefree.