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 ∈ Finset.Ico m n, f i • g i = f (n - 1) • ∑ i ∈ Finset.range n, g i - f m • ∑ i ∈ Finset.range m, g i - ∑ i ∈ Finset.Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ Finset.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 ∈ Finset.Ioc m n, f i • g i = f n • ∑ i ∈ Finset.range (n + 1), g i - f (m + 1) • ∑ i ∈ Finset.range (m + 1), g i - ∑ i ∈ Finset.Ioc m (n - 1), (f (i + 1) - f i) • ∑ i ∈ Finset.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 ∈ Finset.range n, f i • g i = f (n - 1) • ∑ i ∈ Finset.range n, g i - ∑ i ∈ Finset.range (n - 1), (f (i + 1) - f i) • ∑ i ∈ Finset.range (i + 1), g i

Summation by parts for ranges