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.sum (Finset.Ico m n) fun (i : ℕ) => f i • g i) = ((f (n - 1) • Finset.sum (Finset.range n) fun (i : ℕ) => g i) - f m • Finset.sum (Finset.range m) fun (i : ℕ) => g i) - Finset.sum (Finset.Ico m (n - 1)) fun (i : ℕ) =>
(f (i + 1) - f i) • Finset.sum (Finset.range (i + 1)) 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.sum (Finset.range n) fun (i : ℕ) => f i • g i) = (f (n - 1) • Finset.sum (Finset.range n) fun (i : ℕ) => g i) - Finset.sum (Finset.range (n - 1)) fun (i : ℕ) =>
(f (i + 1) - f i) • Finset.sum (Finset.range (i + 1)) fun (i : ℕ) => g i
Summation by parts for ranges