Comparing a Stieltjes-type sum with an integral

An abstract form of the summation by parts in [I71, Lemma 13]: if g is a cumulative counting function that is within ε of F at the points a 0 ≤ a 1 ≤ ⋯ ≤ a n, with F' = f ≥ 0 and increments F (a (j+1)) - F (a j) ≤ δ, then for b ≥ 0 monotone ∑_j b (a (j+1)) (g (j+1) - g j) = ∫ b f + O((δ + 2ε) b (a n)).

theorem IwaniecLinearSieve.abs_sum_mul_sub_le {n : ℕ} {β e : ℕ → ℝ} {ε : ℝ} (hβ : ∀ j < n, β j ≤ β (j + 1)) (hβ0 : 0 ≤ β 0) (he : ∀ j ≤ n, |e j| ≤ ε) : |∑ j ∈ Finset.range n, β (j + 1) * (e (j + 1) - e j)| ≤ 2 * ε * β n

Abel summation bound: if β is nonnegative and monotone and |e j| ≤ ε, then |∑_{j<n} β (j+1) (e (j+1) - e j)| ≤ 2 ε β n.

theorem IwaniecLinearSieve.abs_sum_sub_integral_le {n : ℕ} {a : ℕ → ℝ} (ha : Monotone a) {b f F : ℝ → ℝ} {g : ℕ → ℝ} {δ ε : ℝ} (hδ0 : 0 ≤ δ) (hb : MonotoneOn b (Set.Icc (a 0) (a n))) (hb0 : 0 ≤ b (a 0)) (hf : ∀ x ∈ Set.Icc (a 0) (a n), 0 ≤ f x) (hfc : ContinuousOn f (Set.Icc (a 0) (a n))) (hFf : ∀ j < n, ∫ (x : ℝ) in a j..a (j + 1), f x = F (a (j + 1)) - F (a j)) (hδ : ∀ j < n, F (a (j + 1)) - F (a j) ≤ δ) (hε : ∀ j ≤ n, |g j - F (a j)| ≤ ε) : |∑ j ∈ Finset.range n, b (a (j + 1)) * (g (j + 1) - g j) - ∫ (x : ℝ) in a 0..a n, b x * f x| ≤ (δ + 2 * ε) * b (a n)

Abstract form of [I71, Lemma 13]. The points a 0 ≤ ⋯ ≤ a n partition [a 0, a n]; g j is a cumulative counting function at a j, within ε of F (a j), where F' = f ≥ 0 and F increases by at most δ on each piece. Then for b ≥ 0 monotone, ∑_j b (a (j+1)) (g (j+1) - g j) is within (δ + 2ε) b (a n) of ∫ b f.