Linear convolution error from a power-saving summatory estimate

theorem NairTenenbaum.arithmeticSummatory_mul_finite (a g : ArithmeticFunction ℝ) (x : ℝ) : arithmeticSummatory (⇑(g * a)) x = ∑ d ∈ Finset.Icc 1 ⌊x⌋₊, g d * arithmeticSummatory (⇑a) (x / ↑d)

theorem NairTenenbaum.arithmeticSummatory_convolution_power_error {a g : ArithmeticFunction ℝ} (hg : ∀ (n : ℕ), 0 ≤ g n) {κ E C θ x : ℝ} (hE : 0 ≤ E) (hC : 0 ≤ C) (ha : ∀ (t : ℝ), 1 ≤ t → |arithmeticSummatory (⇑a) t - κ * t| ≤ E * t ^ θ) (hbound : ∀ (t : ℝ), 1 ≤ t → arithmeticSummatory (⇑g) t ≤ C * t) (hθ : 0 ≤ θ) (hθ1 : θ < 1) (hx : 1 ≤ x) : |arithmeticSummatory (⇑(g * a)) x - κ * x * arithmeticSummatory (fun (n : ℕ) => g n / ↑n) x| ≤ E * C / (1 - θ) * x