Summation by parts

theorem Finset.sum_Ico_by_parts {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (f : ℕ → R) (g : ℕ → M) {m n : ℕ} (hmn : m < n) : ∑ i ∈ Ico m n, f i • g i = f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i - ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Summation by parts, also known as Abel's lemma or an Abel transformation

theorem Finset.sum_Ioc_by_parts {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (f : ℕ → R) (g : ℕ → M) {m n : ℕ} (hmn : m < n) : ∑ i ∈ Ioc m n, f i • g i = f n • ∑ i ∈ range (n + 1), g i - f (m + 1) • ∑ i ∈ range (m + 1), g i - ∑ i ∈ Ioc m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

theorem Finset.sum_range_by_parts {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (f : ℕ → R) (g : ℕ → M) (n : ℕ) : ∑ i ∈ range n, f i • g i = f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Summation by parts for ranges

theorem Finset.sum_range_by_parts' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (f : ℕ → R) (g : ℕ → M) (n : ℕ) : ∑ i ∈ range n, f i • g i = (∑ i ∈ range n, f i) • g (n - 1) - ∑ i ∈ range (n - 1), (∑ j ∈ range (i + 1), f j) • (g (i + 1) - g i)

Summation by parts for ranges, differencing the second (module) factor instead of the first: the mirror image of sum_range_by_parts.