Logarithmically weighted sums under a power-saving mean estimate

theorem NairTenenbaum.arithmeticSummatory_log_le_of_power_error {a : ℕ → ℝ} (ha0 : a 0 = 0) (ha : ∀ (n : ℕ), 0 ≤ a n) {κ E θ x : ℝ} (hE : 0 ≤ E) (hbound : arithmeticSummatory a x ≤ κ * x + E * x ^ θ) (hθ : θ < 1) (hx : 1 ≤ x) : arithmeticSummatory (fun (n : ℕ) => a n * Real.log ↑n) x ≤ κ * x * Real.log x + E / (1 - θ) * x