Sums over intervals of natural numbers

A sum ∑ k ∈ range (N + 3), f k whose summands split as f 0 = 0, f 1 = β 1, f k = γ k + β k for 2 ≤ k ≤ N + 1 and f (N + 2) = γ (N + 2) regroups as the sum over 1 ≤ k ≤ N + 1 of the adjacent pairs β k + γ (k + 1). The codomain is any additive commutative monoid. A constant summed over the n - 2 indices 1 ≤ k < n - 1 is (n - 2) times it.

Main results

• Finset.sum_range_eq_sum_Ico_add: the regrouping of ∑ k ∈ range (N + 3), f k into the pairs β k + γ (k + 1).
• Finset.sum_Ico_one_sub_one_const: ∑ _k ∈ Ico 1 (n - 1), c = (n - 2) * c for 2 ≤ n.

theorem Finset.sum_range_eq_sum_Ico_add {M : Type u_1} [AddCommMonoid M] {f β γ : ℕ → M} {N : ℕ} (h₀ : f 0 = 0) (h₁ : f 1 = β 1) (hmid : ∀ k ∈ Ico 2 (N + 2), f k = γ k + β k) (hlast : f (N + 2) = γ (N + 2)) : ∑ k ∈ range (N + 3), f k = ∑ k ∈ Ico 1 (N + 2), (β k + γ (k + 1))

If the summands of a sum over range (N + 3) are f 0 = 0, f 1 = β 1, f k = γ k + β k for 2 ≤ k < N + 2 and f (N + 2) = γ (N + 2), the sum regroups as the sum of the adjacent pairs β k + γ (k + 1) over 1 ≤ k < N + 2.

theorem Finset.sum_Ico_one_sub_one_const {R : Type u_1} [Ring R] {n : ℕ} (hn : 2 ≤ n) (c : R) : ∑ _k ∈ Ico 1 (n - 1), c = (↑n - 2) * c

A constant summed over the n - 2 indices 1 ≤ k < n - 1 is (n - 2) times it.