Removing the squarefree restriction from the Hooley mean

The coprime squarefree/powerful decomposition injects into a product of finite sets. Its powerful weight is summed using the proved convergent series.

theorem NairTenenbaum.hooleyRootWeight_mul_le (Q : Polynomial ℤ) {t : ℝ} (ht : 0 ≤ t) {a b : ℕ} (hab : a.Coprime b) : ↑(hooleyDelta (a * b)) ^ t * (↑(rootCount Q (a * b)) / ↑(a * b)) ≤ ↑a.divisors.card ^ t * ↑(rootCount Q a) / ↑a * (↑(hooleyDelta b) ^ t * ↑(rootCount Q b) / ↑b)

theorem NairTenenbaum.hooleyRootSum_le_powerful_mul_squarefree {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {t : ℝ} (ht : 0 ≤ t) (x : ℝ) : hooleyRootSum Q t x ≤ (∑' (n : { n : ℕ // Powerful n }), powerfulRootWeight Q t n) * squarefreeHooleyRootSum Q t x