The total logarithmic mass with an explicit interval-length error

theorem NairTenenbaum.exists_polynomialLogMass_length_lower_bound {Q : Polynomial ℤ} (hQ : Q ≠ 0) : ∃ (x₀ : ℝ) (B : ℝ), 1 < x₀ ∧ 0 ≤ B ∧ ∀ (x y : ℝ), x₀ < x → 1 ≤ y → ↑Q.natDegree * y * Real.log x - B * y - ↑Q.natDegree * Real.log x ≤ polynomialLogMass Q x y

theorem NairTenenbaum.eventually_log_le_positive_rpow {β : ℝ} (hβ : 0 < β) : ∀ᶠ (x : ℝ) in Filter.atTop, Real.log x ≤ x ^ β

theorem NairTenenbaum.exists_polynomialLogMass_linear_error {Q : Polynomial ℤ} (hQ : Q ≠ 0) {β : ℝ} (hβ : 0 < β) : ∃ (x₀ : ℝ) (B : ℝ), 1 < x₀ ∧ 0 ≤ B ∧ ∀ (x y : ℝ), x₀ < x → x ^ β ≤ y → ↑Q.natDegree * y * Real.log x - B * y ≤ polynomialLogMass Q x y