Finite squarefree Hooley sums with a free moment order

For every eligible q, the reciprocal sum is bounded by a constant times (Kq)^q (log x)^(2^t−t+t/q). The cutoff and constants are independent of q.

theorem NairTenenbaum.exists_squarefreeHooleyRootSum_power_bound {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {t : ℝ} (ht : 1 ≤ t) : ∃ (K : ℝ) (x₀ : ℝ), 1 ≤ K ∧ 1 < x₀ ∧ ∀ (q : ℕ), 2 < q → 2 * t ≤ ↑q → ∀ (x : ℝ), x₀ < x → squarefreeHooleyRootSum Q t x ≤ 2 ^ t * Real.exp 1 * ((K * ↑q) ^ q * Real.log x ^ (2 ^ t - t + t / ↑q))