mathlib3 documentation

algebra.big_operators.intervals

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_Ico_reflect {β : Type v} [comm_monoid β] (f : β) (k : ) {m n : } (h : m n + 1) :
(finset.Ico k m).prod (λ (j : ), f (n - j)) = (finset.Ico (n + 1 - m) (n + 1 - k)).prod (λ (j : ), f j)
theorem finset.sum_Ico_reflect {δ : Type u_1} [add_comm_monoid δ] (f : δ) (k : ) {m n : } (h : m n + 1) :
(finset.Ico k m).sum (λ (j : ), f (n - j)) = (finset.Ico (n + 1 - m) (n + 1 - k)).sum (λ (j : ), f j)
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]
theorem finset.prod_Ico_id_eq_factorial (n : ) :
(finset.Ico 1 (n + 1)).prod (λ (x : ), x) = n.factorial
@[simp]
theorem finset.prod_range_add_one_eq_factorial (n : ) :
(finset.range n).prod (λ (x : ), x + 1) = n.factorial
theorem finset.sum_range_id_mul_two (n : ) :
(finset.range n).sum (λ (i : ), i) * 2 = n * (n - 1)

Gauss' summation formula

theorem finset.sum_range_id (n : ) :
(finset.range n).sum (λ (i : ), i) = n * (n - 1) / 2

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)
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) :
(finset.Ico m n).sum (λ (i : ), f i g i) = f (n - 1) (finset.range n).sum (λ (i : ), g i) - f m (finset.range m).sum (λ (i : ), g i) - (finset.Ico m (n - 1)).sum (λ (i : ), (f (i + 1) - f i) (finset.range (i + 1)).sum (λ (i : ), 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 : ) :
(finset.range n).sum (λ (i : ), f i g i) = f (n - 1) (finset.range n).sum (λ (i : ), g i) - (finset.range (n - 1)).sum (λ (i : ), (f (i + 1) - f i) (finset.range (i + 1)).sum (λ (i : ), g i))

Summation by parts for ranges