The small-prime logarithmic mass with a linear error

theorem NairTenenbaum.exists_polynomialSmoothLogMass_linear_error {Q : Polynomial ℤ} (hQ : Irreducible Q) (hdeg : 0 < Q.natDegree) {β 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 * Real.log y + B * y