Results about big operators over intervals

We prove results about big operators over intervals.

theorem Finset.add_sum_Ico_eq_sum_Icc {α : Type u_1} {M : Type u_2} [PartialOrder α] [AddCommMonoid M] {f : α → M} {a : α} {b : α} [LocallyFiniteOrder α] (h : a ≤ b) : (f b + Finset.sum (Finset.Ico a b) fun (x : α) => f x) = Finset.sum (Finset.Icc a b) fun (x : α) => f x

theorem Finset.mul_prod_Ico_eq_prod_Icc {α : Type u_1} {M : Type u_2} [PartialOrder α] [CommMonoid M] {f : α → M} {a : α} {b : α} [LocallyFiniteOrder α] (h : a ≤ b) : (f b * Finset.prod (Finset.Ico a b) fun (x : α) => f x) = Finset.prod (Finset.Icc a b) fun (x : α) => f x

theorem Finset.sum_Ico_add_eq_sum_Icc {α : Type u_1} {M : Type u_2} [PartialOrder α] [AddCommMonoid M] {f : α → M} {a : α} {b : α} [LocallyFiniteOrder α] (h : a ≤ b) : (Finset.sum (Finset.Ico a b) fun (x : α) => f x) + f b = Finset.sum (Finset.Icc a b) fun (x : α) => f x

theorem Finset.prod_Ico_mul_eq_prod_Icc {α : Type u_1} {M : Type u_2} [PartialOrder α] [CommMonoid M] {f : α → M} {a : α} {b : α} [LocallyFiniteOrder α] (h : a ≤ b) : (Finset.prod (Finset.Ico a b) fun (x : α) => f x) * f b = Finset.prod (Finset.Icc a b) fun (x : α) => f x

theorem Finset.add_sum_Ioc_eq_sum_Icc {α : Type u_1} {M : Type u_2} [PartialOrder α] [AddCommMonoid M] {f : α → M} {a : α} {b : α} [LocallyFiniteOrder α] (h : a ≤ b) : (f a + Finset.sum (Finset.Ioc a b) fun (x : α) => f x) = Finset.sum (Finset.Icc a b) fun (x : α) => f x

theorem Finset.mul_prod_Ioc_eq_prod_Icc {α : Type u_1} {M : Type u_2} [PartialOrder α] [CommMonoid M] {f : α → M} {a : α} {b : α} [LocallyFiniteOrder α] (h : a ≤ b) : (f a * Finset.prod (Finset.Ioc a b) fun (x : α) => f x) = Finset.prod (Finset.Icc a b) fun (x : α) => f x

theorem Finset.sum_Ioc_add_eq_sum_Icc {α : Type u_1} {M : Type u_2} [PartialOrder α] [AddCommMonoid M] {f : α → M} {a : α} {b : α} [LocallyFiniteOrder α] (h : a ≤ b) : (Finset.sum (Finset.Ioc a b) fun (x : α) => f x) + f a = Finset.sum (Finset.Icc a b) fun (x : α) => f x

theorem Finset.prod_Ioc_mul_eq_prod_Icc {α : Type u_1} {M : Type u_2} [PartialOrder α] [CommMonoid M] {f : α → M} {a : α} {b : α} [LocallyFiniteOrder α] (h : a ≤ b) : (Finset.prod (Finset.Ioc a b) fun (x : α) => f x) * f a = Finset.prod (Finset.Icc a b) fun (x : α) => f x

theorem Finset.add_sum_Ioi_eq_sum_Ici {α : Type u_1} {M : Type u_2} [PartialOrder α] [AddCommMonoid M] {f : α → M} [LocallyFiniteOrderTop α] (a : α) : (f a + Finset.sum (Finset.Ioi a) fun (x : α) => f x) = Finset.sum (Finset.Ici a) fun (x : α) => f x

theorem Finset.mul_prod_Ioi_eq_prod_Ici {α : Type u_1} {M : Type u_2} [PartialOrder α] [CommMonoid M] {f : α → M} [LocallyFiniteOrderTop α] (a : α) : (f a * Finset.prod (Finset.Ioi a) fun (x : α) => f x) = Finset.prod (Finset.Ici a) fun (x : α) => f x

theorem Finset.sum_Ioi_add_eq_sum_Ici {α : Type u_1} {M : Type u_2} [PartialOrder α] [AddCommMonoid M] {f : α → M} [LocallyFiniteOrderTop α] (a : α) : (Finset.sum (Finset.Ioi a) fun (x : α) => f x) + f a = Finset.sum (Finset.Ici a) fun (x : α) => f x

theorem Finset.prod_Ioi_mul_eq_prod_Ici {α : Type u_1} {M : Type u_2} [PartialOrder α] [CommMonoid M] {f : α → M} [LocallyFiniteOrderTop α] (a : α) : (Finset.prod (Finset.Ioi a) fun (x : α) => f x) * f a = Finset.prod (Finset.Ici a) fun (x : α) => f x

theorem Finset.add_sum_Iio_eq_sum_Iic {α : Type u_1} {M : Type u_2} [PartialOrder α] [AddCommMonoid M] {f : α → M} [LocallyFiniteOrderBot α] (a : α) : (f a + Finset.sum (Finset.Iio a) fun (x : α) => f x) = Finset.sum (Finset.Iic a) fun (x : α) => f x

theorem Finset.mul_prod_Iio_eq_prod_Iic {α : Type u_1} {M : Type u_2} [PartialOrder α] [CommMonoid M] {f : α → M} [LocallyFiniteOrderBot α] (a : α) : (f a * Finset.prod (Finset.Iio a) fun (x : α) => f x) = Finset.prod (Finset.Iic a) fun (x : α) => f x

theorem Finset.sum_Iio_add_eq_sum_Iic {α : Type u_1} {M : Type u_2} [PartialOrder α] [AddCommMonoid M] {f : α → M} [LocallyFiniteOrderBot α] (a : α) : (Finset.sum (Finset.Iio a) fun (x : α) => f x) + f a = Finset.sum (Finset.Iic a) fun (x : α) => f x

theorem Finset.prod_Iio_mul_eq_prod_Iic {α : Type u_1} {M : Type u_2} [PartialOrder α] [CommMonoid M] {f : α → M} [LocallyFiniteOrderBot α] (a : α) : (Finset.prod (Finset.Iio a) fun (x : α) => f x) * f a = Finset.prod (Finset.Iic a) fun (x : α) => f x

theorem Finset.sum_Ico_add' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (f : α → M) (a : α) (b : α) (c : α) : (Finset.sum (Finset.Ico a b) fun (x : α) => f (x + c)) = Finset.sum (Finset.Ico (a + c) (b + c)) fun (x : α) => f x

theorem Finset.prod_Ico_add' {α : Type u_1} {M : Type u_2} [CommMonoid M] [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (f : α → M) (a : α) (b : α) (c : α) : (Finset.prod (Finset.Ico a b) fun (x : α) => f (x + c)) = Finset.prod (Finset.Ico (a + c) (b + c)) fun (x : α) => f x

theorem Finset.sum_Ico_add {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (f : α → M) (a : α) (b : α) (c : α) : (Finset.sum (Finset.Ico a b) fun (x : α) => f (c + x)) = Finset.sum (Finset.Ico (a + c) (b + c)) fun (x : α) => f x

theorem Finset.prod_Ico_add {α : Type u_1} {M : Type u_2} [CommMonoid M] [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (f : α → M) (a : α) (b : α) (c : α) : (Finset.prod (Finset.Ico a b) fun (x : α) => f (c + x)) = Finset.prod (Finset.Ico (a + c) (b + c)) fun (x : α) => f x

theorem Finset.sum_Ico_succ_top {M : Type u_2} [AddCommMonoid M] {a : ℕ} {b : ℕ} (hab : a ≤ b) (f : ℕ → M) : (Finset.sum (Finset.Ico a (b + 1)) fun (k : ℕ) => f k) = (Finset.sum (Finset.Ico a b) fun (k : ℕ) => f k) + f b

theorem Finset.prod_Ico_succ_top {M : Type u_2} [CommMonoid M] {a : ℕ} {b : ℕ} (hab : a ≤ b) (f : ℕ → M) : (Finset.prod (Finset.Ico a (b + 1)) fun (k : ℕ) => f k) = (Finset.prod (Finset.Ico a b) fun (k : ℕ) => f k) * f b

theorem Finset.sum_eq_sum_Ico_succ_bot {M : Type u_2} [AddCommMonoid M] {a : ℕ} {b : ℕ} (hab : a < b) (f : ℕ → M) : (Finset.sum (Finset.Ico a b) fun (k : ℕ) => f k) = f a + Finset.sum (Finset.Ico (a + 1) b) fun (k : ℕ) => f k

theorem Finset.prod_eq_prod_Ico_succ_bot {M : Type u_2} [CommMonoid M] {a : ℕ} {b : ℕ} (hab : a < b) (f : ℕ → M) : (Finset.prod (Finset.Ico a b) fun (k : ℕ) => f k) = f a * Finset.prod (Finset.Ico (a + 1) b) fun (k : ℕ) => f k

theorem Finset.sum_Ico_consecutive {M : Type u_2} [AddCommMonoid M] (f : ℕ → M) {m : ℕ} {n : ℕ} {k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : ((Finset.sum (Finset.Ico m n) fun (i : ℕ) => f i) + Finset.sum (Finset.Ico n k) fun (i : ℕ) => f i) = Finset.sum (Finset.Ico m k) fun (i : ℕ) => f i

theorem Finset.prod_Ico_consecutive {M : Type u_2} [CommMonoid M] (f : ℕ → M) {m : ℕ} {n : ℕ} {k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : ((Finset.prod (Finset.Ico m n) fun (i : ℕ) => f i) * Finset.prod (Finset.Ico n k) fun (i : ℕ) => f i) = Finset.prod (Finset.Ico m k) fun (i : ℕ) => f i

theorem Finset.sum_Ioc_consecutive {M : Type u_2} [AddCommMonoid M] (f : ℕ → M) {m : ℕ} {n : ℕ} {k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : ((Finset.sum (Finset.Ioc m n) fun (i : ℕ) => f i) + Finset.sum (Finset.Ioc n k) fun (i : ℕ) => f i) = Finset.sum (Finset.Ioc m k) fun (i : ℕ) => f i

theorem Finset.prod_Ioc_consecutive {M : Type u_2} [CommMonoid M] (f : ℕ → M) {m : ℕ} {n : ℕ} {k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : ((Finset.prod (Finset.Ioc m n) fun (i : ℕ) => f i) * Finset.prod (Finset.Ioc n k) fun (i : ℕ) => f i) = Finset.prod (Finset.Ioc m k) fun (i : ℕ) => f i

theorem Finset.sum_Ioc_succ_top {M : Type u_2} [AddCommMonoid M] {a : ℕ} {b : ℕ} (hab : a ≤ b) (f : ℕ → M) : (Finset.sum (Finset.Ioc a (b + 1)) fun (k : ℕ) => f k) = (Finset.sum (Finset.Ioc a b) fun (k : ℕ) => f k) + f (b + 1)

theorem Finset.prod_Ioc_succ_top {M : Type u_2} [CommMonoid M] {a : ℕ} {b : ℕ} (hab : a ≤ b) (f : ℕ → M) : (Finset.prod (Finset.Ioc a (b + 1)) fun (k : ℕ) => f k) = (Finset.prod (Finset.Ioc a b) fun (k : ℕ) => f k) * f (b + 1)

theorem Finset.sum_range_add_sum_Ico {M : Type u_2} [AddCommMonoid M] (f : ℕ → M) {m : ℕ} {n : ℕ} (h : m ≤ n) : ((Finset.sum (Finset.range m) fun (k : ℕ) => f k) + Finset.sum (Finset.Ico m n) fun (k : ℕ) => f k) = Finset.sum (Finset.range n) fun (k : ℕ) => f k

theorem Finset.prod_range_mul_prod_Ico {M : Type u_2} [CommMonoid M] (f : ℕ → M) {m : ℕ} {n : ℕ} (h : m ≤ n) : ((Finset.prod (Finset.range m) fun (k : ℕ) => f k) * Finset.prod (Finset.Ico m n) fun (k : ℕ) => f k) = Finset.prod (Finset.range n) fun (k : ℕ) => f k

theorem Finset.sum_Ico_eq_add_neg {δ : Type u_3} [AddCommGroup δ] (f : ℕ → δ) {m : ℕ} {n : ℕ} (h : m ≤ n) : (Finset.sum (Finset.Ico m n) fun (k : ℕ) => f k) = (Finset.sum (Finset.range n) fun (k : ℕ) => f k) + -Finset.sum (Finset.range m) fun (k : ℕ) => f k

theorem Finset.prod_Ico_eq_mul_inv {δ : Type u_3} [CommGroup δ] (f : ℕ → δ) {m : ℕ} {n : ℕ} (h : m ≤ n) : (Finset.prod (Finset.Ico m n) fun (k : ℕ) => f k) = (Finset.prod (Finset.range n) fun (k : ℕ) => f k) * (Finset.prod (Finset.range m) fun (k : ℕ) => f k)⁻¹

theorem Finset.sum_Ico_eq_sub {δ : Type u_3} [AddCommGroup δ] (f : ℕ → δ) {m : ℕ} {n : ℕ} (h : m ≤ n) : (Finset.sum (Finset.Ico m n) fun (k : ℕ) => f k) = (Finset.sum (Finset.range n) fun (k : ℕ) => f k) - Finset.sum (Finset.range m) fun (k : ℕ) => f k

theorem Finset.prod_Ico_eq_div {δ : Type u_3} [CommGroup δ] (f : ℕ → δ) {m : ℕ} {n : ℕ} (h : m ≤ n) : (Finset.prod (Finset.Ico m n) fun (k : ℕ) => f k) = (Finset.prod (Finset.range n) fun (k : ℕ) => f k) / Finset.prod (Finset.range m) fun (k : ℕ) => f k

theorem Finset.sum_range_sub_sum_range {α : Type u_3} [AddCommGroup α] {f : ℕ → α} {n : ℕ} {m : ℕ} (hnm : n ≤ m) : ((Finset.sum (Finset.range m) fun (k : ℕ) => f k) - Finset.sum (Finset.range n) fun (k : ℕ) => f k) = Finset.sum (Finset.filter (fun (k : ℕ) => n ≤ k) (Finset.range m)) fun (k : ℕ) => f k

theorem Finset.prod_range_div_prod_range {α : Type u_3} [CommGroup α] {f : ℕ → α} {n : ℕ} {m : ℕ} (hnm : n ≤ m) : ((Finset.prod (Finset.range m) fun (k : ℕ) => f k) / Finset.prod (Finset.range n) fun (k : ℕ) => f k) = Finset.prod (Finset.filter (fun (k : ℕ) => n ≤ k) (Finset.range m)) fun (k : ℕ) => f k

theorem Finset.sum_Ico_Ico_comm {M : Type u_3} [AddCommMonoid M] (a : ℕ) (b : ℕ) (f : ℕ → ℕ → M) : (Finset.sum (Finset.Ico a b) fun (i : ℕ) => Finset.sum (Finset.Ico i b) fun (j : ℕ) => f i j) = Finset.sum (Finset.Ico a b) fun (j : ℕ) => Finset.sum (Finset.Ico a (j + 1)) fun (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 {M : Type u_2} [AddCommMonoid M] (f : ℕ → M) (m : ℕ) (n : ℕ) : (Finset.sum (Finset.Ico m n) fun (k : ℕ) => f k) = Finset.sum (Finset.range (n - m)) fun (k : ℕ) => f (m + k)

theorem Finset.prod_Ico_eq_prod_range {M : Type u_2} [CommMonoid M] (f : ℕ → M) (m : ℕ) (n : ℕ) : (Finset.prod (Finset.Ico m n) fun (k : ℕ) => f k) = Finset.prod (Finset.range (n - m)) fun (k : ℕ) => f (m + k)

theorem Finset.prod_Ico_reflect {M : Type u_2} [CommMonoid M] (f : ℕ → M) (k : ℕ) {m : ℕ} {n : ℕ} (h : m ≤ n + 1) : (Finset.prod (Finset.Ico k m) fun (j : ℕ) => f (n - j)) = Finset.prod (Finset.Ico (n + 1 - m) (n + 1 - k)) fun (j : ℕ) => f j

theorem Finset.sum_Ico_reflect {δ : Type u_3} [AddCommMonoid δ] (f : ℕ → δ) (k : ℕ) {m : ℕ} {n : ℕ} (h : m ≤ n + 1) : (Finset.sum (Finset.Ico k m) fun (j : ℕ) => f (n - j)) = Finset.sum (Finset.Ico (n + 1 - m) (n + 1 - k)) fun (j : ℕ) => f j

theorem Finset.prod_range_reflect {M : Type u_2} [CommMonoid M] (f : ℕ → M) (n : ℕ) : (Finset.prod (Finset.range n) fun (j : ℕ) => f (n - 1 - j)) = Finset.prod (Finset.range n) fun (j : ℕ) => f j

theorem Finset.sum_range_reflect {δ : Type u_3} [AddCommMonoid δ] (f : ℕ → δ) (n : ℕ) : (Finset.sum (Finset.range n) fun (j : ℕ) => f (n - 1 - j)) = Finset.sum (Finset.range n) fun (j : ℕ) => f j

@[simp]

theorem Finset.prod_Ico_id_eq_factorial (n : ℕ) : (Finset.prod (Finset.Ico 1 (n + 1)) fun (x : ℕ) => x) = Nat.factorial n

@[simp]

theorem Finset.prod_range_add_one_eq_factorial (n : ℕ) : (Finset.prod (Finset.range n) fun (x : ℕ) => x + 1) = Nat.factorial n

theorem Finset.sum_range_id_mul_two (n : ℕ) : (Finset.sum (Finset.range n) fun (i : ℕ) => i) * 2 = n * (n - 1)

Gauss' summation formula

theorem Finset.sum_range_id (n : ℕ) : (Finset.sum (Finset.range n) fun (i : ℕ) => i) = n * (n - 1) / 2

Gauss' summation formula

theorem Finset.sum_range_succ_sub_sum {M : Type u_3} (f : ℕ → M) {n : ℕ} [AddCommGroup M] : ((Finset.sum (Finset.range (n + 1)) fun (i : ℕ) => f i) - Finset.sum (Finset.range n) fun (i : ℕ) => f i) = f n

theorem Finset.prod_range_succ_div_prod {M : Type u_3} (f : ℕ → M) {n : ℕ} [CommGroup M] : ((Finset.prod (Finset.range (n + 1)) fun (i : ℕ) => f i) / Finset.prod (Finset.range n) fun (i : ℕ) => f i) = f n

theorem Finset.sum_range_succ_sub_top {M : Type u_3} (f : ℕ → M) {n : ℕ} [AddCommGroup M] : (Finset.sum (Finset.range (n + 1)) fun (i : ℕ) => f i) - f n = Finset.sum (Finset.range n) fun (i : ℕ) => f i

theorem Finset.prod_range_succ_div_top {M : Type u_3} (f : ℕ → M) {n : ℕ} [CommGroup M] : (Finset.prod (Finset.range (n + 1)) fun (i : ℕ) => f i) / f n = Finset.prod (Finset.range n) fun (i : ℕ) => f i

theorem Finset.sum_Ico_sub_bot {M : Type u_3} (f : ℕ → M) {m : ℕ} {n : ℕ} [AddCommGroup M] (hmn : m < n) : (Finset.sum (Finset.Ico m n) fun (i : ℕ) => f i) - f m = Finset.sum (Finset.Ico (m + 1) n) fun (i : ℕ) => f i

theorem Finset.prod_Ico_div_bot {M : Type u_3} (f : ℕ → M) {m : ℕ} {n : ℕ} [CommGroup M] (hmn : m < n) : (Finset.prod (Finset.Ico m n) fun (i : ℕ) => f i) / f m = Finset.prod (Finset.Ico (m + 1) n) fun (i : ℕ) => f i

theorem Finset.sum_Ico_succ_sub_top {M : Type u_3} (f : ℕ → M) {m : ℕ} {n : ℕ} [AddCommGroup M] (hmn : m ≤ n) : (Finset.sum (Finset.Ico m (n + 1)) fun (i : ℕ) => f i) - f n = Finset.sum (Finset.Ico m n) fun (i : ℕ) => f i

theorem Finset.prod_Ico_succ_div_top {M : Type u_3} (f : ℕ → M) {m : ℕ} {n : ℕ} [CommGroup M] (hmn : m ≤ n) : (Finset.prod (Finset.Ico m (n + 1)) fun (i : ℕ) => f i) / f n = Finset.prod (Finset.Ico m n) fun (i : ℕ) => f i

theorem Finset.sum_Ico_by_parts {R : Type u_3} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] (f : ℕ → R) (g : ℕ → M) {m : ℕ} {n : ℕ} (hmn : m < n) : (Finset.sum (Finset.Ico m n) fun (i : ℕ) => f i • g i) = ((f (n - 1) • Finset.sum (Finset.range n) fun (i : ℕ) => g i) - f m • Finset.sum (Finset.range m) fun (i : ℕ) => g i) - Finset.sum (Finset.Ico m (n - 1)) fun (i : ℕ) => (f (i + 1) - f i) • Finset.sum (Finset.range (i + 1)) fun (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_3} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] (f : ℕ → R) (g : ℕ → M) (n : ℕ) : (Finset.sum (Finset.range n) fun (i : ℕ) => f i • g i) = (f (n - 1) • Finset.sum (Finset.range n) fun (i : ℕ) => g i) - Finset.sum (Finset.range (n - 1)) fun (i : ℕ) => (f (i + 1) - f i) • Finset.sum (Finset.range (i + 1)) fun (i : ℕ) => g i

Summation by parts for ranges