Finset.sum_range_by_parts
theorem Finset.sum_range_by_parts :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : 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
This theorem is a version of the "summation by parts" formula, adapted for the range of natural numbers less than some value `n`. For any ring `R` and a commutative group with addition `M` over which `R` is a module, and given two functions `f` from the natural numbers to `R` and `g` from the natural numbers to `M`, the theorem states that the sum over the range of `n` of `f(i)` scaled by `g(i)` is equal to `f(n - 1)` scaled by the sum of `g(i)` over the range of `n` minus the sum over the range of `n - 1` of the difference `f(i + 1) - f(i)` scaled by the sum of `g(i)` over the range of `i + 1`.
More concisely: For any ring R and commutative group M with addition, for functions f from the natural numbers to R and g from the natural numbers to M, the sum from i = 0 to n-1 of f(i) * g(i) equals f(n-1) * sum from i = 0 to n-1 g(i) - sum from i = 0 to n-2 g(i+1) * (f(i+1) - f(i)).
|
Finset.sum_Ico_by_parts
theorem Finset.sum_Ico_by_parts :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : ℕ → R)
(g : ℕ → M) {m n : ℕ},
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
This theorem, known as the Summation by parts, Abel's lemma, or Abel transformation, states that for any Ring `R` and AddCommGroup `M` with a Module structure over `R`, and for any functions `f : ℕ → R` and `g : ℕ → M`, if we have two natural numbers `m` and `n` with `m < n`, then the sum from `m` to `n` (exclusive) of the product of `f(i)` and `g(i)` is equal to the difference of (1) the product of `f(n-1)` and the sum of `g(i)` for `i` in the range `n`, and `f(m)` and the sum of `g(i)` for `i` in the range `m`, and (2) the sum from `m` to `n-1` (exclusive) of the product of the difference between `f(i+1)` and `f(i)` and the sum of `g(i)` for `i` in the range `i+1`. This theorem is a version of integration by parts for sums.
More concisely: For any ring `R`, additive commutative group `M` with an `R`-module structure, functions `f : ℕ → R` and `g : ℕ → M`, the sum from `m` to `n-1` (exclusive) of `f(i) * g(i)` equals `f(n-1) * g(n) - f(m) * g(m) - Σ[i=m..n-2] (f(i+1)-f(i)) * g(i)`.
|