Hooley moments without the no-fixed-prime-divisor restriction

A logarithmic exponent margin absorbs the subexponential factor. The interval range y ≤ x/2 suffices for the power-shaped intervals in Theorem 2.

theorem NairTenenbaum.exists_hooleyPolynomialSum_log_margin_unrestricted {Q : Polynomial ℤ} (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {t α δ : ℝ} (ht : 1 ≤ t) (hα : 0 < α) (hδ : 0 < δ) : ∃ (x₀ : ℝ) (C : ℝ), 1 < x₀ ∧ 0 < C ∧ ∀ (x y : ℝ), x₀ < x → x ^ α ≤ y → y ≤ x / 2 → hooleyPolynomialSum Q t x y ≤ C * y * Real.log x ^ (2 ^ t - t - 1 + δ)