Results about big operators over intervals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 : α) :
(finset.Ico a b).prod (λ (x : α), f (x + c)) = (finset.Ico (a + c) (b + c)).prod (λ (x : α), 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 : α) :
(finset.Ico a b).sum (λ (x : α), f (x + c)) = (finset.Ico (a + c) (b + c)).sum (λ (x : α), 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 : α) :
(finset.Ico a b).sum (λ (x : α), f (c + x)) = (finset.Ico (a + c) (b + c)).sum (λ (x : α), 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 : α) :
(finset.Ico a b).prod (λ (x : α), f (c + x)) = (finset.Ico (a + c) (b + c)).prod (λ (x : α), f x)
theorem
finset.sum_Ico_succ_top
{δ : Type u_1}
[add_comm_monoid δ]
{a b : ℕ}
(hab : a ≤ b)
(f : ℕ → δ) :
(finset.Ico a (b + 1)).sum (λ (k : ℕ), f k) = (finset.Ico a b).sum (λ (k : ℕ), f k) + f b
theorem
finset.prod_Ico_succ_top
{β : Type v}
[comm_monoid β]
{a b : ℕ}
(hab : a ≤ b)
(f : ℕ → β) :
(finset.Ico a (b + 1)).prod (λ (k : ℕ), f k) = (finset.Ico a b).prod (λ (k : ℕ), f k) * f b
theorem
finset.sum_eq_sum_Ico_succ_bot
{δ : Type u_1}
[add_comm_monoid δ]
{a b : ℕ}
(hab : a < b)
(f : ℕ → δ) :
(finset.Ico a b).sum (λ (k : ℕ), f k) = f a + (finset.Ico (a + 1) b).sum (λ (k : ℕ), f k)
theorem
finset.prod_eq_prod_Ico_succ_bot
{β : Type v}
[comm_monoid β]
{a b : ℕ}
(hab : a < b)
(f : ℕ → β) :
(finset.Ico a b).prod (λ (k : ℕ), f k) = f a * (finset.Ico (a + 1) b).prod (λ (k : ℕ), f k)
theorem
finset.sum_Ico_consecutive
{β : Type v}
[add_comm_monoid β]
(f : ℕ → β)
{m n k : ℕ}
(hmn : m ≤ n)
(hnk : n ≤ k) :
(finset.Ico m n).sum (λ (i : ℕ), f i) + (finset.Ico n k).sum (λ (i : ℕ), f i) = (finset.Ico m k).sum (λ (i : ℕ), f i)
theorem
finset.prod_Ico_consecutive
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
{m n k : ℕ}
(hmn : m ≤ n)
(hnk : n ≤ k) :
(finset.Ico m n).prod (λ (i : ℕ), f i) * (finset.Ico n k).prod (λ (i : ℕ), f i) = (finset.Ico m k).prod (λ (i : ℕ), f i)
theorem
finset.prod_Ioc_consecutive
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
{m n k : ℕ}
(hmn : m ≤ n)
(hnk : n ≤ k) :
(finset.Ioc m n).prod (λ (i : ℕ), f i) * (finset.Ioc n k).prod (λ (i : ℕ), f i) = (finset.Ioc m k).prod (λ (i : ℕ), f i)
theorem
finset.sum_Ioc_consecutive
{β : Type v}
[add_comm_monoid β]
(f : ℕ → β)
{m n k : ℕ}
(hmn : m ≤ n)
(hnk : n ≤ k) :
(finset.Ioc m n).sum (λ (i : ℕ), f i) + (finset.Ioc n k).sum (λ (i : ℕ), f i) = (finset.Ioc m k).sum (λ (i : ℕ), f i)
theorem
finset.sum_Ioc_succ_top
{β : Type v}
[add_comm_monoid β]
{a b : ℕ}
(hab : a ≤ b)
(f : ℕ → β) :
(finset.Ioc a (b + 1)).sum (λ (k : ℕ), f k) = (finset.Ioc a b).sum (λ (k : ℕ), f k) + f (b + 1)
theorem
finset.prod_Ioc_succ_top
{β : Type v}
[comm_monoid β]
{a b : ℕ}
(hab : a ≤ b)
(f : ℕ → β) :
(finset.Ioc a (b + 1)).prod (λ (k : ℕ), f k) = (finset.Ioc a b).prod (λ (k : ℕ), f k) * f (b + 1)
theorem
finset.prod_range_mul_prod_Ico
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
{m n : ℕ}
(h : m ≤ n) :
(finset.range m).prod (λ (k : ℕ), f k) * (finset.Ico m n).prod (λ (k : ℕ), f k) = (finset.range n).prod (λ (k : ℕ), f k)
theorem
finset.sum_range_add_sum_Ico
{β : Type v}
[add_comm_monoid β]
(f : ℕ → β)
{m n : ℕ}
(h : m ≤ n) :
(finset.range m).sum (λ (k : ℕ), f k) + (finset.Ico m n).sum (λ (k : ℕ), f k) = (finset.range n).sum (λ (k : ℕ), f k)
theorem
finset.prod_Ico_eq_mul_inv
{δ : Type u_1}
[comm_group δ]
(f : ℕ → δ)
{m n : ℕ}
(h : m ≤ n) :
(finset.Ico m n).prod (λ (k : ℕ), f k) = (finset.range n).prod (λ (k : ℕ), f k) * ((finset.range m).prod (λ (k : ℕ), f k))⁻¹
theorem
finset.sum_Ico_eq_add_neg
{δ : Type u_1}
[add_comm_group δ]
(f : ℕ → δ)
{m n : ℕ}
(h : m ≤ n) :
(finset.Ico m n).sum (λ (k : ℕ), f k) = (finset.range n).sum (λ (k : ℕ), f k) + -(finset.range m).sum (λ (k : ℕ), f k)
theorem
finset.sum_Ico_eq_sub
{δ : Type u_1}
[add_comm_group δ]
(f : ℕ → δ)
{m n : ℕ}
(h : m ≤ n) :
(finset.Ico m n).sum (λ (k : ℕ), f k) = (finset.range n).sum (λ (k : ℕ), f k) - (finset.range m).sum (λ (k : ℕ), f k)
theorem
finset.prod_Ico_eq_div
{δ : Type u_1}
[comm_group δ]
(f : ℕ → δ)
{m n : ℕ}
(h : m ≤ n) :
(finset.Ico m n).prod (λ (k : ℕ), f k) = (finset.range n).prod (λ (k : ℕ), f k) / (finset.range m).prod (λ (k : ℕ), f k)
theorem
finset.sum_range_sub_sum_range
{α : Type u_1}
[add_comm_group α]
{f : ℕ → α}
{n m : ℕ}
(hnm : n ≤ m) :
(finset.range m).sum (λ (k : ℕ), f k) - (finset.range n).sum (λ (k : ℕ), f k) = (finset.filter (λ (k : ℕ), n ≤ k) (finset.range m)).sum (λ (k : ℕ), f k)
theorem
finset.prod_range_sub_prod_range
{α : Type u_1}
[comm_group α]
{f : ℕ → α}
{n m : ℕ}
(hnm : n ≤ m) :
(finset.range m).prod (λ (k : ℕ), f k) / (finset.range n).prod (λ (k : ℕ), f k) = (finset.filter (λ (k : ℕ), n ≤ k) (finset.range m)).prod (λ (k : ℕ), f k)
theorem
finset.sum_Ico_Ico_comm
{M : Type u_1}
[add_comm_monoid M]
(a b : ℕ)
(f : ℕ → ℕ → M) :
(finset.Ico a b).sum (λ (i : ℕ), (finset.Ico i b).sum (λ (j : ℕ), f i j)) = (finset.Ico a b).sum (λ (j : ℕ), (finset.Ico a (j + 1)).sum (λ (i : ℕ), 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 : ℕ) :
(finset.Ico m n).sum (λ (k : ℕ), f k) = (finset.range (n - m)).sum (λ (k : ℕ), f (m + k))
theorem
finset.prod_Ico_eq_prod_range
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
(m n : ℕ) :
(finset.Ico m n).prod (λ (k : ℕ), f k) = (finset.range (n - m)).prod (λ (k : ℕ), f (m + k))
theorem
finset.prod_range_reflect
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
(finset.range n).prod (λ (j : ℕ), f (n - 1 - j)) = (finset.range n).prod (λ (j : ℕ), f j)
theorem
finset.sum_range_reflect
{δ : Type u_1}
[add_comm_monoid δ]
(f : ℕ → δ)
(n : ℕ) :
(finset.range n).sum (λ (j : ℕ), f (n - 1 - j)) = (finset.range n).sum (λ (j : ℕ), f j)
@[simp]
@[simp]
Gauss' summation formula
Gauss' summation formula
theorem
finset.prod_range_succ_div_prod
{β : Type u_1}
(f : ℕ → β)
{n : ℕ}
[comm_group β] :
(finset.range (n + 1)).prod (λ (i : ℕ), f i) / (finset.range n).prod (λ (i : ℕ), f i) = f n
theorem
finset.sum_range_succ_sub_sum
{β : Type u_1}
(f : ℕ → β)
{n : ℕ}
[add_comm_group β] :
(finset.range (n + 1)).sum (λ (i : ℕ), f i) - (finset.range n).sum (λ (i : ℕ), f i) = f n
theorem
finset.prod_range_succ_div_top
{β : Type u_1}
(f : ℕ → β)
{n : ℕ}
[comm_group β] :
(finset.range (n + 1)).prod (λ (i : ℕ), f i) / f n = (finset.range n).prod (λ (i : ℕ), f i)
theorem
finset.sum_range_succ_sub_top
{β : Type u_1}
(f : ℕ → β)
{n : ℕ}
[add_comm_group β] :
(finset.range (n + 1)).sum (λ (i : ℕ), f i) - f n = (finset.range n).sum (λ (i : ℕ), f i)
theorem
finset.prod_Ico_div_bot
{β : Type u_1}
(f : ℕ → β)
{m n : ℕ}
[comm_group β]
(hmn : m < n) :
(finset.Ico m n).prod (λ (i : ℕ), f i) / f m = (finset.Ico (m + 1) n).prod (λ (i : ℕ), f i)
theorem
finset.sum_Ico_sub_bot
{β : Type u_1}
(f : ℕ → β)
{m n : ℕ}
[add_comm_group β]
(hmn : m < n) :
(finset.Ico m n).sum (λ (i : ℕ), f i) - f m = (finset.Ico (m + 1) n).sum (λ (i : ℕ), f i)
theorem
finset.prod_Ico_succ_div_top
{β : Type u_1}
(f : ℕ → β)
{m n : ℕ}
[comm_group β]
(hmn : m ≤ n) :
(finset.Ico m (n + 1)).prod (λ (i : ℕ), f i) / f n = (finset.Ico m n).prod (λ (i : ℕ), f i)
theorem
finset.sum_Ico_succ_sub_top
{β : Type u_1}
(f : ℕ → β)
{m n : ℕ}
[add_comm_group β]
(hmn : m ≤ n) :
(finset.Ico m (n + 1)).sum (λ (i : ℕ), f i) - f n = (finset.Ico m n).sum (λ (i : ℕ), f i)