Results about big operators over intervals
We prove results about big operators over intervals (mostly the ℕ-valued Ico m n).
theorem
finset.sum_Ico_add
{δ : Type u_1}
[add_comm_monoid δ]
(f : ℕ → δ)
(m n k : ℕ) :
∑ (l : ℕ) in finset.Ico m n, f (k + l) = ∑ (l : ℕ) in finset.Ico (m + k) (n + k), f l
theorem
finset.prod_Ico_add
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
(m n k : ℕ) :
∏ (l : ℕ) in finset.Ico m n, f (k + l) = ∏ (l : ℕ) in finset.Ico (m + k) (n + k), f l
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.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]
Gauss' summation formula
Gauss' summation formula