Results about big operators over intervals #
We prove results about big operators over intervals (mostly the ℕ-valued Ico m n).
theorem
finset.prod_Ico_add'
{α : Type u}
{β : Type v}
[comm_monoid β]
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(f : α → β)
(a b c : α) :
∏ (x : α) in finset.Ico a b, f (x + c) = ∏ (x : α) in finset.Ico (a + c) (b + c), f x
theorem
finset.sum_Ico_add'
{α : Type u}
{β : Type v}
[add_comm_monoid β]
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(f : α → β)
(a b c : α) :
∑ (x : α) in finset.Ico a b, f (x + c) = ∑ (x : α) in finset.Ico (a + c) (b + c), f x
theorem
finset.sum_Ico_add
{α : Type u}
{β : Type v}
[add_comm_monoid β]
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(f : α → β)
(a b c : α) :
∑ (x : α) in finset.Ico a b, f (c + x) = ∑ (x : α) in finset.Ico (a + c) (b + c), f x
theorem
finset.prod_Ico_add
{α : Type u}
{β : Type v}
[comm_monoid β]
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(f : α → β)
(a b c : α) :
∏ (x : α) in finset.Ico a b, f (c + x) = ∏ (x : α) in finset.Ico (a + c) (b + c), f x
theorem
finset.sum_Ico_succ_top
{δ : Type u_1}
[add_comm_monoid δ]
{a b : ℕ}
(hab : a ≤ b)
(f : ℕ → δ) :
∑ (k : ℕ) in finset.Ico a (b + 1), f k = ∑ (k : ℕ) in finset.Ico a b, f k + f b
theorem
finset.prod_Ico_succ_top
{β : Type v}
[comm_monoid β]
{a b : ℕ}
(hab : a ≤ b)
(f : ℕ → β) :
∏ (k : ℕ) in finset.Ico a (b + 1), f k = (∏ (k : ℕ) in finset.Ico a b, f k) * f b
theorem
finset.sum_eq_sum_Ico_succ_bot
{δ : Type u_1}
[add_comm_monoid δ]
{a b : ℕ}
(hab : a < b)
(f : ℕ → δ) :
∑ (k : ℕ) in finset.Ico a b, f k = f a + ∑ (k : ℕ) in finset.Ico (a + 1) b, f k
theorem
finset.prod_eq_prod_Ico_succ_bot
{β : Type v}
[comm_monoid β]
{a b : ℕ}
(hab : a < b)
(f : ℕ → β) :
∏ (k : ℕ) in finset.Ico a b, f k = (f a) * ∏ (k : ℕ) in finset.Ico (a + 1) b, f k
theorem
finset.sum_Ico_consecutive
{β : Type v}
[add_comm_monoid β]
(f : ℕ → β)
{m n k : ℕ}
(hmn : m ≤ n)
(hnk : n ≤ k) :
∑ (i : ℕ) in finset.Ico m n, f i + ∑ (i : ℕ) in finset.Ico n k, f i = ∑ (i : ℕ) in finset.Ico m k, f i
theorem
finset.prod_Ico_consecutive
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
{m n k : ℕ}
(hmn : m ≤ n)
(hnk : n ≤ k) :
(∏ (i : ℕ) in finset.Ico m n, f i) * ∏ (i : ℕ) in finset.Ico n k, f i = ∏ (i : ℕ) in finset.Ico m k, f i
theorem
finset.prod_range_mul_prod_Ico
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
{m n : ℕ}
(h : m ≤ n) :
(∏ (k : ℕ) in finset.range m, f k) * ∏ (k : ℕ) in finset.Ico m n, f k = ∏ (k : ℕ) in finset.range n, f k
theorem
finset.sum_range_add_sum_Ico
{β : Type v}
[add_comm_monoid β]
(f : ℕ → β)
{m n : ℕ}
(h : m ≤ n) :
∑ (k : ℕ) in finset.range m, f k + ∑ (k : ℕ) in finset.Ico m n, f k = ∑ (k : ℕ) in finset.range n, f k
theorem
finset.prod_Ico_eq_mul_inv
{δ : Type u_1}
[comm_group δ]
(f : ℕ → δ)
{m n : ℕ}
(h : m ≤ n) :
∏ (k : ℕ) in finset.Ico m n, f k = (∏ (k : ℕ) in finset.range n, f k) * (∏ (k : ℕ) in finset.range m, f k)⁻¹
theorem
finset.sum_Ico_eq_add_neg
{δ : Type u_1}
[add_comm_group δ]
(f : ℕ → δ)
{m n : ℕ}
(h : m ≤ n) :
∑ (k : ℕ) in finset.Ico m n, f k = ∑ (k : ℕ) in finset.range n, f k + -∑ (k : ℕ) in finset.range m, f k
theorem
finset.sum_Ico_eq_sub
{δ : Type u_1}
[add_comm_group δ]
(f : ℕ → δ)
{m n : ℕ}
(h : m ≤ n) :
∑ (k : ℕ) in finset.Ico m n, f k = ∑ (k : ℕ) in finset.range n, f k - ∑ (k : ℕ) in finset.range m, f k
theorem
finset.prod_Ico_eq_div
{δ : Type u_1}
[comm_group δ]
(f : ℕ → δ)
{m n : ℕ}
(h : m ≤ n) :
∏ (k : ℕ) in finset.Ico m n, f k = (∏ (k : ℕ) in finset.range n, f k) / ∏ (k : ℕ) in finset.range m, f k
theorem
finset.sum_range_sub_sum_range
{α : Type u_1}
[add_comm_group α]
{f : ℕ → α}
{n m : ℕ}
(hnm : n ≤ m) :
∑ (k : ℕ) in finset.range m, f k - ∑ (k : ℕ) in finset.range n, f k = ∑ (k : ℕ) in finset.filter (λ (k : ℕ), n ≤ k) (finset.range m), f k
theorem
finset.prod_range_sub_prod_range
{α : Type u_1}
[comm_group α]
{f : ℕ → α}
{n m : ℕ}
(hnm : n ≤ m) :
(∏ (k : ℕ) in finset.range m, f k) / ∏ (k : ℕ) in finset.range n, f k = ∏ (k : ℕ) in finset.filter (λ (k : ℕ), n ≤ k) (finset.range m), f k
theorem
finset.sum_Ico_Ico_comm
{M : Type u_1}
[add_comm_monoid M]
(a b : ℕ)
(f : ℕ → ℕ → M) :
∑ (i : ℕ) in finset.Ico a b, ∑ (j : ℕ) in finset.Ico i b, f i j = ∑ (j : ℕ) in finset.Ico a b, ∑ (i : ℕ) in finset.Ico a (j + 1), f i j
The two ways of summing over (i,j) in the range a<=i<=j<b are equal.
theorem
finset.sum_Ico_eq_sum_range
{β : Type v}
[add_comm_monoid β]
(f : ℕ → β)
(m n : ℕ) :
∑ (k : ℕ) in finset.Ico m n, f k = ∑ (k : ℕ) in finset.range (n - m), f (m + k)
theorem
finset.prod_Ico_eq_prod_range
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
(m n : ℕ) :
∏ (k : ℕ) in finset.Ico m n, f k = ∏ (k : ℕ) in finset.range (n - m), f (m + k)
theorem
finset.prod_Ico_reflect
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
(k : ℕ)
{m n : ℕ}
(h : m ≤ n + 1) :
∏ (j : ℕ) in finset.Ico k m, f (n - j) = ∏ (j : ℕ) in finset.Ico (n + 1 - m) (n + 1 - k), f j
theorem
finset.sum_Ico_reflect
{δ : Type u_1}
[add_comm_monoid δ]
(f : ℕ → δ)
(k : ℕ)
{m n : ℕ}
(h : m ≤ n + 1) :
∑ (j : ℕ) in finset.Ico k m, f (n - j) = ∑ (j : ℕ) in finset.Ico (n + 1 - m) (n + 1 - k), f j
theorem
finset.prod_range_reflect
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
∏ (j : ℕ) in finset.range n, f (n - 1 - j) = ∏ (j : ℕ) in finset.range n, f j
theorem
finset.sum_range_reflect
{δ : Type u_1}
[add_comm_monoid δ]
(f : ℕ → δ)
(n : ℕ) :
∑ (j : ℕ) in finset.range n, f (n - 1 - j) = ∑ (j : ℕ) in finset.range n, f j
@[simp]
@[simp]
Gauss' summation formula
Gauss' summation formula
theorem
finset.prod_range_succ_div_prod
{β : Type u_1}
(f : ℕ → β)
{n : ℕ}
[comm_group β] :
(∏ (i : ℕ) in finset.range (n + 1), f i) / ∏ (i : ℕ) in finset.range n, f i = f n
theorem
finset.sum_range_succ_sub_sum
{β : Type u_1}
(f : ℕ → β)
{n : ℕ}
[add_comm_group β] :
∑ (i : ℕ) in finset.range (n + 1), f i - ∑ (i : ℕ) in finset.range n, f i = f n
theorem
finset.prod_range_succ_div_top
{β : Type u_1}
(f : ℕ → β)
{n : ℕ}
[comm_group β] :
(∏ (i : ℕ) in finset.range (n + 1), f i) / f n = ∏ (i : ℕ) in finset.range n, f i
theorem
finset.sum_range_succ_sub_top
{β : Type u_1}
(f : ℕ → β)
{n : ℕ}
[add_comm_group β] :
∑ (i : ℕ) in finset.range (n + 1), f i - f n = ∑ (i : ℕ) in finset.range n, f i
theorem
finset.prod_Ico_div_bot
{β : Type u_1}
(f : ℕ → β)
{m n : ℕ}
[comm_group β]
(hmn : m < n) :
(∏ (i : ℕ) in finset.Ico m n, f i) / f m = ∏ (i : ℕ) in finset.Ico (m + 1) n, f i
theorem
finset.sum_Ico_sub_bot
{β : Type u_1}
(f : ℕ → β)
{m n : ℕ}
[add_comm_group β]
(hmn : m < n) :
∑ (i : ℕ) in finset.Ico m n, f i - f m = ∑ (i : ℕ) in finset.Ico (m + 1) n, f i
theorem
finset.prod_Ico_succ_div_top
{β : Type u_1}
(f : ℕ → β)
{m n : ℕ}
[comm_group β]
(hmn : m ≤ n) :
(∏ (i : ℕ) in finset.Ico m (n + 1), f i) / f n = ∏ (i : ℕ) in finset.Ico m n, f i
theorem
finset.sum_Ico_succ_sub_top
{β : Type u_1}
(f : ℕ → β)
{m n : ℕ}
[add_comm_group β]
(hmn : m ≤ n) :
∑ (i : ℕ) in finset.Ico m (n + 1), f i - f n = ∑ (i : ℕ) in finset.Ico m n, f i
theorem
finset.sum_Ico_by_parts
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(f : ℕ → R)
(g : ℕ → M)
{m n : ℕ}
(hmn : m < n) :
∑ (i : ℕ) in finset.Ico m n, f i • g i = f (n - 1) • ∑ (i : ℕ) in finset.range n, g i - f m • ∑ (i : ℕ) in finset.range m, g i - ∑ (i : ℕ) in finset.Ico m (n - 1), (f (i + 1) - f i) • ∑ (i : ℕ) in 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]
[add_comm_group M]
[module R M]
(f : ℕ → R)
(g : ℕ → M)
(n : ℕ) :
∑ (i : ℕ) in finset.range n, f i • g i = f (n - 1) • ∑ (i : ℕ) in finset.range n, g i - ∑ (i : ℕ) in finset.range (n - 1), (f (i + 1) - f i) • ∑ (i : ℕ) in finset.range (i + 1), g i
Summation by parts for ranges