Comparing weighted sums through their partial sums

If every initial partial sum of f is at most the corresponding partial sum of g, then the same comparison holds after weighting both sequences by a nonnegative, antitone weight w: ∑_{i < N} w i * f i ≤ ∑_{i < N} w i * g i. This is Abel's inequality in its comparison form. Summation by parts (Finset.sum_range_by_parts) writes the difference of the two weighted sums as the last weight times the last partial-sum difference plus the successive decrements of w times the earlier partial-sum differences, and every one of these products is nonnegative.

No sign condition on f or g is needed. The typical use takes g constant: a bound ∑_{i < k} f i ≤ k • C on all partial sums then gives ∑ w i * f i ≤ (∑ w i) * C for every nonnegative antitone weight.

Main results

• TauCeti.sum_range_mul_le_sum_range_mul: the weighted comparison.

theorem TauCeti.sum_range_mul_le_sum_range_mul {R : Type u_1} [Ring R] [Preorder R] [IsOrderedAddMonoid R] [PosMulMono R] {f g w : ℕ → R} {N : ℕ} (hfg : ∀ k ≤ N, ∑ i ∈ Finset.range k, f i ≤ ∑ i ∈ Finset.range k, g i) (hw : ∀ (i : ℕ), i + 1 < N → w (i + 1) ≤ w i) (hw0 : 0 ≤ w (N - 1)) : ∑ i ∈ Finset.range N, w i * f i ≤ ∑ i ∈ Finset.range N, w i * g i

Abel's inequality, comparison form. If the partial sums of f are dominated by those of g up to N, and w is nonnegative and antitone on the first N indices, then ∑_{i < N} w i * f i ≤ ∑_{i < N} w i * g i. Only the last weight is required to be nonnegative explicitly; the other signs follow from the successive comparisons when N > 0.