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 : ℕ) :
(finset.Ico m n).sum (λ (l : ℕ), f (k + l)) = (finset.Ico (m + k) (n + k)).sum (λ (l : ℕ), f l)
theorem
finset.prod_Ico_add
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
(m n k : ℕ) :
(finset.Ico m n).prod (λ (l : ℕ), f (k + l)) = (finset.Ico (m + k) (n + k)).prod (λ (l : ℕ), f l)
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.prod_Ico_consecutive
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
{m n k : ℕ} :
m ≤ n → 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.sum_Ico_consecutive
{β : Type v}
[add_comm_monoid β]
(f : ℕ → β)
{m n k : ℕ} :
m ≤ n → 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.sum_range_add_sum_Ico
{β : Type v}
[add_comm_monoid β]
(f : ℕ → β)
{m n : ℕ} :
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_range_mul_prod_Ico
{β : Type v}
[comm_monoid β]
(f : ℕ → β)
{m n : ℕ} :
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_Ico_eq_add_neg
{δ : Type u_1}
[add_comm_group δ]
(f : ℕ → δ)
{m n : ℕ} :
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_mul_inv
{δ : Type u_1}
[comm_group δ]
(f : ℕ → δ)
{m n : ℕ} :
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_sub
{δ : Type u_1}
[add_comm_group δ]
(f : ℕ → δ)
{m n : ℕ} :
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_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.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_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]
Gauss' summation formula
Gauss' summation formula