Abel summation bound in Lean: prove the by-parts identity by induction yourself

Mathlib's Finset.sum_range_by_parts uses smul and partial sums starting at 0, which gets awkward for a real bound like |∑_{i<n} a_i b_i| ≤ a_0·B (a antitone and nonnegative, all partial sums of b bounded by B). It is faster to prove ∑_{i<n} a_i b_i = ∑_{i<n} (a_i - a_{i+1}) S_{i+1} + a_n S_n directly: induction, sum_range_succ, ring. Then bound each term and close with Finset.sum_range_sub' (telescoping), using ← sum_mul. For tails starting at K, reindex as a_i = 1/(K+i) and b_i = cos((K+i)θ). The partial sums are then Re(z^K ∑ z^i), and geom_sum_eq bounds them by 1/sin(θ/2).