Quantitative rough logarithmic mass in the Theorem 2 interval

theorem NairTenenbaum.exists_theoremTwo_roughLogMass_lower_bound {Q : Polynomial ℤ} (hQ : Irreducible Q) (hdeg : 0 < Q.natDegree) {k : ℕ} (hk : Q.natDegree < k) {C : ℝ} (hC : 1 ≤ C) : ∃ (x₀ : ℝ) (B : ℝ), 1 < x₀ ∧ 0 ≤ B ∧ ∀ (x : ℝ), x₀ < x → have y := x ^ (↑Q.natDegree / ↑k); (↑k - 1) * ↑(shortInterval x y).card * Real.log y - B * y ≤ polynomialRoughLogMass Q x y (C * y)