Partial summation for real arithmetic summatory functions

theorem NairTenenbaum.arithmeticSummatory_eq_sum_Icc_zero {a : ℕ → ℝ} (ha : a 0 = 0) (x : ℝ) : arithmeticSummatory a x = ∑ n ∈ Finset.Icc 0 ⌊x⌋₊, a n

theorem NairTenenbaum.arithmeticSummatory_mono {a : ℕ → ℝ} (ha : ∀ (n : ℕ), 0 ≤ a n) : Monotone (arithmeticSummatory a)

theorem NairTenenbaum.arithmeticSummatory_mul_eq_sub_integral {a : ℕ → ℝ} (ha : a 0 = 0) {f g : ℝ → ℝ} {x : ℝ} (hx : 1 ≤ x) (hd : ∀ t ∈ Set.Icc 1 x, HasDerivAt f (g t) t) (hc : ContinuousOn g (Set.Icc 1 x)) : arithmeticSummatory (fun (n : ℕ) => f ↑n * a n) x = f x * arithmeticSummatory a x - ∫ (t : ℝ) in 1..x, g t * arithmeticSummatory a t