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_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