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)
:
((Finset.Ico m n).sum fun (i : ℕ) => f i • g i) = ((f (n - 1) • (Finset.range n).sum fun (i : ℕ) => g i) - f m • (Finset.range m).sum fun (i : ℕ) => g i) - (Finset.Ico m (n - 1)).sum fun (i : ℕ) => (f (i + 1) - f i) • (Finset.range (i + 1)).sum fun (i : ℕ) => g i
Summation by parts, also known as Abel's lemma or an Abel transformation
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 : ℕ)
:
((Finset.range n).sum fun (i : ℕ) => f i • g i) = (f (n - 1) • (Finset.range n).sum fun (i : ℕ) => g i) - (Finset.range (n - 1)).sum fun (i : ℕ) => (f (i + 1) - f i) • (Finset.range (i + 1)).sum fun (i : ℕ) => g i
Summation by parts for ranges