Small-prime logarithmic mass reduced to the weighted prime-root sum

theorem NairTenenbaum.exists_polynomialSmoothLogMass_prime_bound {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) (hD : Q.discr ≠ 0) {β C : ℝ} (hβ : 0 < β) (hC : 1 ≤ C) : ∃ (x₀ : ℝ) (B : ℝ), 1 < x₀ ∧ 0 ≤ B ∧ ∀ (x y : ℝ), x₀ < x → x ^ β ≤ y → y ≤ x → polynomialSmoothLogMass Q x y (C * y) ≤ (y + 1) * primeRootLogSum Q (C * y) + B * y