Root counts under arithmetic-progression substitution

The affine map is a permutation modulo every modulus coprime to its slope. At a prime dividing the slope, the transformed polynomial is constant. These facts supply the root-count identities in the proof of Corollary 1.

noncomputable def NairTenenbaum.affinePolynomial (q : ℕ) (a : ℤ) : Polynomial ℤ

The integral substitution used to parametrize a residue class.

Equations

• NairTenenbaum.affinePolynomial q a = Polynomial.C ↑q * Polynomial.X + Polynomial.C a

@[simp]

theorem NairTenenbaum.eval_affinePolynomial (q : ℕ) (a t : ℤ) : Polynomial.eval t (affinePolynomial q a) = ↑q * t + a

@[simp]

theorem NairTenenbaum.eval₂_affinePolynomial {R : Type u_1} [CommRing R] (q : ℕ) (a : ℤ) (t : R) : Polynomial.eval₂ (Int.castRingHom R) t (affinePolynomial q a) = ↑q * t + ↑a

noncomputable def NairTenenbaum.rootsAffine (Q : Polynomial ℤ) (q : ℕ) (a : ℤ) (n : ℕ) (hqn : q.Coprime n) : ResidueRoots (Q.comp (affinePolynomial q a)) n ≃ ResidueRoots Q n

The residue-root equivalence induced by an invertible affine substitution.

Equations

• NairTenenbaum.rootsAffine Q q a n hqn = (Equiv.trans ⋯.unit.mulLeft (Equiv.addRight ↑a)).subtypeEquiv ⋯

theorem NairTenenbaum.rootCount_comp_affine_of_coprime (Q : Polynomial ℤ) (q : ℕ) (a : ℤ) (n : ℕ) (hqn : q.Coprime n) : rootCount (Q.comp (affinePolynomial q a)) n = rootCount Q n

Equation (37)'s substitution preserves root counts at coprime moduli.

theorem NairTenenbaum.rootCount_comp_affine_prime_eq_zero (Q : Polynomial ℤ) {q p : ℕ} (a : ℤ) (hpq : p ∣ q) (hpa : ¬p ∣ (Polynomial.eval a Q).natAbs) : rootCount (Q.comp (affinePolynomial q a)) p = 0

At a prime dividing the slope, the value at the residue representative controls every root of the transformed polynomial.

theorem NairTenenbaum.rootCount_comp_affine_eq_zero (Q : Polynomial ℤ) (q : ℕ) (a : ℤ) (n : ℕ) (hqa : q.Coprime (Polynomial.eval a Q).natAbs) (hqn : ¬q.Coprime n) : rootCount (Q.comp (affinePolynomial q a)) n = 0

Under the progression's coprimality hypothesis, every modulus sharing a prime with the slope has no roots.

theorem NairTenenbaum.rootCount_comp_affine (Q : Polynomial ℤ) (q : ℕ) (a : ℤ) (n : ℕ) (hqa : q.Coprime (Polynomial.eval a Q).natAbs) : rootCount (Q.comp (affinePolynomial q a)) n = if q.Coprime n then rootCount Q n else 0

The full root-count formula, including all prime powers and composite moduli.

theorem NairTenenbaum.NoFixedPrimeDivisor.comp_affine {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (q : ℕ) (a : ℤ) (hqa : q.Coprime (Polynomial.eval a Q).natAbs) : NoFixedPrimeDivisor (Q.comp (affinePolynomial q a))

A permitted arithmetic progression preserves absence of fixed prime divisors, as required when applying Theorem 1 to the substituted family.

noncomputable def NairTenenbaum.progressionSieveProduct (Q : Polynomial ℤ) (q : ℕ) (x : ℝ) : ℝ

The Euler product in the arithmetic-progression corollaries omits primes that divide the progression modulus.

Equations

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

theorem NairTenenbaum.sieveProduct_comp_affine (Q : Polynomial ℤ) (q : ℕ) (a : ℤ) (x : ℝ) (hqa : q.Coprime (Polynomial.eval a Q).natAbs) : sieveProduct (Q.comp (affinePolynomial q a)) x = progressionSieveProduct Q q x

The sieve product for the substituted polynomial is exactly the original product with primes dividing the progression modulus omitted.