Local properties of the irreducible polynomial factors

The prime-power bounds outside the restricted bad discriminant, and the discriminant divisibility that controls common divisors of two distinct factors.

theorem NairTenenbaum.PolynomialSystem.factor_dvd_radical {k r : ℕ} (P : PolynomialSystem k r) (h : Fin r) : P.R h ∣ P.radical

theorem NairTenenbaum.PolynomialSystem.two_factors_dvd_radical {k r : ℕ} (P : PolynomialSystem k r) {i j : Fin r} (hij : i ≠ j) : P.R i * P.R j ∣ P.radical

theorem NairTenenbaum.PolynomialSystem.common_value_gcd_dvd_discriminant {k r : ℕ} (P : PolynomialSystem k r) {i j : Fin r} (hij : i ≠ j) (n : ℤ) : (Polynomial.eval n (P.R i)).natAbs.gcd (Polynomial.eval n (P.R j)).natAbs ∣ P.discriminant

theorem NairTenenbaum.PolynomialSystem.prime_dvd_badDiscriminant_iff {k r : ℕ} (P : PolynomialSystem k r) {p : ℕ} (hp : Nat.Prime p) : p ∣ P.badDiscriminant ↔ p ∣ P.discriminant ∧ rootCount P.total p ≠ 0

theorem NairTenenbaum.PolynomialSystem.badDiscriminant_factorization {k r : ℕ} (P : PolynomialSystem k r) (p : ℕ) : P.badDiscriminant.factorization p = if rootCount P.total p = 0 then 0 else P.discriminant.factorization p

theorem NairTenenbaum.PolynomialSystem.factor_rootCount_prime_pow_le {k r : ℕ} (P : PolynomialSystem k r) {p ν : ℕ} (hp : Nat.Prime p) (hν : ν ≠ 0) (hD : ¬p ∣ P.discriminant) (h : Fin r) : rootCount (P.R h) (p ^ ν) ≤ rootCount (P.R h) p

theorem NairTenenbaum.PolynomialSystem.factor_rootCount_prime_pow_le_of_not_dvd_bad {k r : ℕ} (P : PolynomialSystem k r) {p ν : ℕ} (hp : Nat.Prime p) (hν : ν ≠ 0) (hD : ¬p ∣ P.badDiscriminant) (h : Fin r) : rootCount (P.R h) (p ^ ν) ≤ rootCount (P.R h) p

Outside the restricted bad discriminant D, the root counts at every positive prime power are bounded by the number of roots modulo the prime.

theorem NairTenenbaum.PolynomialSystem.factor_rootCount_prime_pow_le_degree {k r : ℕ} (P : PolynomialSystem k r) {p ν : ℕ} (hp : Nat.Prime p) (hν : ν ≠ 0) (hD : ¬p ∣ P.badDiscriminant) (h : Fin r) : rootCount (P.R h) (p ^ ν) ≤ (P.R h).natDegree

theorem NairTenenbaum.PolynomialSystem.radical_rootCount_prime_pow_le_bad_cube {k r : ℕ} (P : PolynomialSystem k r) {p : ℕ} (hp : Nat.Prime p) (hD : p ∣ P.badDiscriminant) (ν : ℕ) : rootCount P.radical (p ^ ν) ≤ P.badDiscriminant ^ 3

A coarse but uniform bound at every prime dividing D.

theorem NairTenenbaum.PolynomialSystem.factor_rootCount_prime_pow_le_bad_cube {k r : ℕ} (P : PolynomialSystem k r) {p : ℕ} (hp : Nat.Prime p) (hD : p ∣ P.badDiscriminant) (ν : ℕ) (h : Fin r) : rootCount (P.R h) (p ^ ν) ≤ P.badDiscriminant ^ 3

The same bad-prime bound applies to every irreducible factor.

theorem NairTenenbaum.PolynomialSystem.factor_rootCount_prime_pow_uniform {k r : ℕ} (P : PolynomialSystem k r) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) (h : Fin r) : rootCount (P.R h) (p ^ ν) ≤ max (P.R h).natDegree (P.badDiscriminant ^ 3)

A bound valid at all prime powers, with no dependence on the coefficients other than through the specified restricted discriminant.