mathlib documentation

algebra.big_operators.intervals

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 : } :
m nn 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 : } :
m nn 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 : } :
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 : } :
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 : } :
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 : } :
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 : } :
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 : } :
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 : } :
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]
theorem finset.prod_Ico_id_eq_factorial (n : ) :
∏ (x : ) in finset.Ico 1 (n + 1), x = n!

@[simp]
theorem finset.prod_range_add_one_eq_factorial (n : ) :
∏ (x : ) in finset.range n, (x + 1) = n!

theorem finset.sum_range_id_mul_two (n : ) :
(∑ (i : ) in finset.range n, i) * 2 = n * (n - 1)

Gauss' summation formula

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

Gauss' summation formula