Absorbing the subexponential factor into a logarithmic margin

theorem NairTenenbaum.hooley_short_exponent_nonneg {t : ℝ} (ht : 1 ≤ t) : 0 ≤ 2 ^ t - t - 1

theorem NairTenenbaum.exists_hooleyPolynomialSum_log_margin {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (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 → hooleyPolynomialSum Q t x y ≤ C * y * Real.log x ^ (2 ^ t - t - 1 + δ)