Equality of residue-root counts under integral normalization

theorem NairTenenbaum.rootCount_integralNormalization_le {Q : Polynomial ℤ} (hdeg : 1 ≤ Q.natDegree) {p : ℕ} (hp : Nat.Prime p) (hgood : ¬p ∣ Q.leadingCoeff.natAbs) : rootCount Q.integralNormalization p ≤ rootCount Q p

theorem NairTenenbaum.rootCount_integralNormalization_eq {Q : Polynomial ℤ} (hdeg : 1 ≤ Q.natDegree) {p : ℕ} (hp : Nat.Prime p) (hgood : ¬p ∣ Q.leadingCoeff.natAbs) : rootCount Q.integralNormalization p = rootCount Q p

theorem NairTenenbaum.primeRootSum_integralNormalization_le_add {Q : Polynomial ℤ} (hdeg : 1 ≤ Q.natDegree) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) {σ : ℝ} (hσ : 1 ≤ σ) : ∑ p ∈ S, ↑(rootCount Q.integralNormalization p) * ↑p ^ (-σ) ≤ ∑ p ∈ S, ↑(rootCount Q p) * ↑p ^ (-σ) + ↑Q.leadingCoeff.natAbs.primeFactors.card

theorem NairTenenbaum.rootPrimePowerSum_integralNormalization_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hdeg : 1 ≤ Q.natDegree) {σ : ℝ} (hσ : 1 < σ) : rootPrimePowerSum Q.integralNormalization σ ≤ rootPrimePowerSum Q σ + ↑Q.leadingCoeff.natAbs.primeFactors.card