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).

source
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)
source
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)
source
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)
source
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)
source
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
source
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
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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))⁻¹
source
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)
source
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)
source
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)
source
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)
source
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)
source
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.

source
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))
source
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))
source
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)
source
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)
source
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)
source
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)
source
@[simp]
theorem finset.prod_Ico_id_eq_factorial (n : ℕ) :
(finset.Ico 1 (n + 1)).prod (λ (x : ℕ), x) = n.factorial
source
@[simp]
theorem finset.prod_range_add_one_eq_factorial (n : ℕ) :
(finset.range n).prod (λ (x : ℕ), x + 1) = n.factorial
source
theorem finset.sum_range_id_mul_two (n : ℕ) :
(finset.range n).sum (λ (i : ℕ), i) * 2 = n * (n - 1)

Gauss' summation formula

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

Gauss' summation formula

source
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
source
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
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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

source
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