Root counts at primes dividing the discriminant

Taylor expansion and the discriminant identity bound the clustering of roots. The resulting count is uniform in the exponent of the modulus.

theorem NairTenenbaum.prime_pow_dvd_of_mul_not_dvd {p x y : ℤ} (hp : Prime p) (a b : ℕ) (hxy : p ^ (a + b) ∣ x * y) (hy : ¬p ^ (b + 1) ∣ y) : p ^ a ∣ x

theorem NairTenenbaum.derivative_not_dvd_of_discr {Q : Polynomial ℤ} (hdeg : 2 ≤ Q.natDegree) {p : ℤ} {δ ν : ℕ} (hδν : δ < ν) (hD : ¬p ^ (δ + 1) ∣ Q.discr) {a : ℤ} (ha : p ^ ν ∣ Polynomial.eval a Q) : ¬p ^ (δ + 1) ∣ Polynomial.eval a (Polynomial.derivative Q)

A root modulo a sufficiently large prime power cannot have its derivative divisible by a higher power than the discriminant allows.

theorem NairTenenbaum.root_difference_dvd_of_discr {Q : Polynomial ℤ} (hdeg : 2 ≤ Q.natDegree) {p : ℤ} (hp : Prime p) {δ ν : ℕ} (hδν : δ < ν) (hD : ¬p ^ (δ + 1) ∣ Q.discr) {a b : ℤ} (ha : p ^ ν ∣ Polynomial.eval a Q) (hb : p ^ ν ∣ Polynomial.eval b Q) (hab : p ^ (δ + 1) ∣ b - a) : p ^ (ν - δ) ∣ b - a

Roots that agree modulo p^(δ+1) agree modulo p^(ν-δ), provided p^(δ+1) does not divide the discriminant.

theorem NairTenenbaum.ResidueRoots.modulus_dvd_eval_val {Q : Polynomial ℤ} {q : ℕ} [NeZero q] (a : ResidueRoots Q q) : ↑q ∣ Polynomial.eval (↑(↑a).val) Q

theorem NairTenenbaum.rootCount_prime_pow_le_discr_bound {Q : Polynomial ℤ} (hdeg : 2 ≤ Q.natDegree) {p : ℕ} (hp : Nat.Prime p) (δ ν : ℕ) (hD : ¬↑p ^ (δ + 1) ∣ Q.discr) : rootCount Q (p ^ ν) ≤ p ^ (2 * δ + 1)

An exponent-independent root bound, with explicit dependence on a power that does not divide the discriminant.

theorem NairTenenbaum.rootCount_prime_pow_le_factorization_bound {Q : Polynomial ℤ} (hdeg : 2 ≤ Q.natDegree) (hD : Q.discr ≠ 0) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : rootCount Q (p ^ ν) ≤ p ^ (2 * Q.discr.natAbs.factorization p + 1)