# 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} [] [] {f : αM} {a : α} {b : α} (h : a b) :
f b + x, f x = x, f x
theorem Finset.mul_prod_Ico_eq_prod_Icc {α : Type u_1} {M : Type u_2} [] [] {f : αM} {a : α} {b : α} (h : a b) :
f b * x, f x = x, f x
theorem Finset.sum_Ico_add_eq_sum_Icc {α : Type u_1} {M : Type u_2} [] [] {f : αM} {a : α} {b : α} (h : a b) :
x, f x + f b = x, f x
theorem Finset.prod_Ico_mul_eq_prod_Icc {α : Type u_1} {M : Type u_2} [] [] {f : αM} {a : α} {b : α} (h : a b) :
(∏ x, f x) * f b = x, f x
theorem Finset.add_sum_Ioc_eq_sum_Icc {α : Type u_1} {M : Type u_2} [] [] {f : αM} {a : α} {b : α} (h : a b) :
f a + x, f x = x, f x
theorem Finset.mul_prod_Ioc_eq_prod_Icc {α : Type u_1} {M : Type u_2} [] [] {f : αM} {a : α} {b : α} (h : a b) :
f a * x, f x = x, f x
theorem Finset.sum_Ioc_add_eq_sum_Icc {α : Type u_1} {M : Type u_2} [] [] {f : αM} {a : α} {b : α} (h : a b) :
x, f x + f a = x, f x
theorem Finset.prod_Ioc_mul_eq_prod_Icc {α : Type u_1} {M : Type u_2} [] [] {f : αM} {a : α} {b : α} (h : a b) :
(∏ x, f x) * f a = x, f x
theorem Finset.add_sum_Ioi_eq_sum_Ici {α : Type u_1} {M : Type u_2} [] [] {f : αM} (a : α) :
f a + x, f x = x, f x
theorem Finset.mul_prod_Ioi_eq_prod_Ici {α : Type u_1} {M : Type u_2} [] [] {f : αM} (a : α) :
f a * x, f x = x, f x
theorem Finset.sum_Ioi_add_eq_sum_Ici {α : Type u_1} {M : Type u_2} [] [] {f : αM} (a : α) :
x, f x + f a = x, f x
theorem Finset.prod_Ioi_mul_eq_prod_Ici {α : Type u_1} {M : Type u_2} [] [] {f : αM} (a : α) :
(∏ x, f x) * f a = x, f x
theorem Finset.add_sum_Iio_eq_sum_Iic {α : Type u_1} {M : Type u_2} [] [] {f : αM} (a : α) :
f a + x, f x = x, f x
theorem Finset.mul_prod_Iio_eq_prod_Iic {α : Type u_1} {M : Type u_2} [] [] {f : αM} (a : α) :
f a * x, f x = x, f x
theorem Finset.sum_Iio_add_eq_sum_Iic {α : Type u_1} {M : Type u_2} [] [] {f : αM} (a : α) :
x, f x + f a = x, f x
theorem Finset.prod_Iio_mul_eq_prod_Iic {α : Type u_1} {M : Type u_2} [] [] {f : αM} (a : α) :
(∏ x, f x) * f a = x, f x
theorem Finset.sum_sum_Ioi_add_eq_sum_sum_off_diag {α : Type u_1} {M : Type u_2} [] [] [] (f : ααM) :
i : α, j, (f j i + f i j) = i : α, j{i}, f j i
theorem Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag {α : Type u_1} {M : Type u_2} [] [] [] (f : ααM) :
i : α, j, f j i * f i j = i : α, j{i}, f j i
theorem Finset.sum_Ico_add' {α : Type u_1} {M : Type u_2} [] [] (f : αM) (a : α) (b : α) (c : α) :
x, f (x + c) = xFinset.Ico (a + c) (b + c), f x
theorem Finset.prod_Ico_add' {α : Type u_1} {M : Type u_2} [] [] (f : αM) (a : α) (b : α) (c : α) :
x, f (x + c) = xFinset.Ico (a + c) (b + c), f x
theorem Finset.sum_Ico_add {α : Type u_1} {M : Type u_2} [] [] (f : αM) (a : α) (b : α) (c : α) :
x, f (c + x) = xFinset.Ico (a + c) (b + c), f x
theorem Finset.prod_Ico_add {α : Type u_1} {M : Type u_2} [] [] (f : αM) (a : α) (b : α) (c : α) :
x, f (c + x) = xFinset.Ico (a + c) (b + c), f x
theorem Finset.sum_Ico_succ_top {M : Type u_2} [] {a : } {b : } (hab : a b) (f : M) :
kFinset.Ico a (b + 1), f k = k, f k + f b
theorem Finset.prod_Ico_succ_top {M : Type u_2} [] {a : } {b : } (hab : a b) (f : M) :
kFinset.Ico a (b + 1), f k = (∏ k, f k) * f b
theorem Finset.sum_eq_sum_Ico_succ_bot {M : Type u_2} [] {a : } {b : } (hab : a < b) (f : M) :
k, f k = f a + kFinset.Ico (a + 1) b, f k
theorem Finset.prod_eq_prod_Ico_succ_bot {M : Type u_2} [] {a : } {b : } (hab : a < b) (f : M) :
k, f k = f a * kFinset.Ico (a + 1) b, f k
theorem Finset.sum_Ico_consecutive {M : Type u_2} [] (f : M) {m : } {n : } {k : } (hmn : m n) (hnk : n k) :
i, f i + i, f i = i, f i
theorem Finset.prod_Ico_consecutive {M : Type u_2} [] (f : M) {m : } {n : } {k : } (hmn : m n) (hnk : n k) :
(∏ i, f i) * i, f i = i, f i
theorem Finset.sum_Ioc_consecutive {M : Type u_2} [] (f : M) {m : } {n : } {k : } (hmn : m n) (hnk : n k) :
i, f i + i, f i = i, f i
theorem Finset.prod_Ioc_consecutive {M : Type u_2} [] (f : M) {m : } {n : } {k : } (hmn : m n) (hnk : n k) :
(∏ i, f i) * i, f i = i, f i
theorem Finset.sum_Ioc_succ_top {M : Type u_2} [] {a : } {b : } (hab : a b) (f : M) :
kFinset.Ioc a (b + 1), f k = k, f k + f (b + 1)
theorem Finset.prod_Ioc_succ_top {M : Type u_2} [] {a : } {b : } (hab : a b) (f : M) :
kFinset.Ioc a (b + 1), f k = (∏ k, f k) * f (b + 1)
theorem Finset.sum_Icc_succ_top {M : Type u_2} [] {a : } {b : } (hab : a b + 1) (f : M) :
kFinset.Icc a (b + 1), f k = k, f k + f (b + 1)
theorem Finset.prod_Icc_succ_top {M : Type u_2} [] {a : } {b : } (hab : a b + 1) (f : M) :
kFinset.Icc a (b + 1), f k = (∏ k, f k) * f (b + 1)
theorem Finset.sum_range_add_sum_Ico {M : Type u_2} [] (f : M) {m : } {n : } (h : m n) :
k, f k + k, f k = k, f k
theorem Finset.prod_range_mul_prod_Ico {M : Type u_2} [] (f : M) {m : } {n : } (h : m n) :
(∏ k, f k) * k, f k = k, f k
theorem Finset.sum_Ico_eq_add_neg {δ : Type u_3} [] (f : δ) {m : } {n : } (h : m n) :
k, f k = k, f k + -k, f k
theorem Finset.prod_Ico_eq_mul_inv {δ : Type u_3} [] (f : δ) {m : } {n : } (h : m n) :
k, f k = (∏ k, f k) * (∏ k, f k)⁻¹
theorem Finset.sum_Ico_eq_sub {δ : Type u_3} [] (f : δ) {m : } {n : } (h : m n) :
k, f k = k, f k - k, f k
theorem Finset.prod_Ico_eq_div {δ : Type u_3} [] (f : δ) {m : } {n : } (h : m n) :
k, f k = (∏ k, f k) / k, f k
theorem Finset.sum_range_sub_sum_range {α : Type u_3} [] {f : α} {n : } {m : } (hnm : n m) :
k, f k - k, f k = kFinset.filter (fun (k : ) => n k) (Finset.range m), f k
theorem Finset.prod_range_div_prod_range {α : Type u_3} [] {f : α} {n : } {m : } (hnm : n m) :
(∏ k, f k) / k, f k = kFinset.filter (fun (k : ) => n k) (Finset.range m), f k
theorem Finset.sum_Ico_Ico_comm {M : Type u_3} [] (a : ) (b : ) (f : M) :
i, j, f i j = j, iFinset.Ico a (j + 1), f i j

The two ways of summing over (i, j) in the range a ≤ i ≤ j < b are equal.

theorem Finset.sum_Ico_Ico_comm' {M : Type u_3} [] (a : ) (b : ) (f : M) :
i, jFinset.Ico (i + 1) b, f i j = j, 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} [] (f : M) (m : ) (n : ) :
k, f k = kFinset.range (n - m), f (m + k)
theorem Finset.prod_Ico_eq_prod_range {M : Type u_2} [] (f : M) (m : ) (n : ) :
k, f k = kFinset.range (n - m), f (m + k)
theorem Finset.prod_Ico_reflect {M : Type u_2} [] (f : M) (k : ) {m : } {n : } (h : m n + 1) :
j, f (n - j) = jFinset.Ico (n + 1 - m) (n + 1 - k), f j
theorem Finset.sum_Ico_reflect {δ : Type u_3} [] (f : δ) (k : ) {m : } {n : } (h : m n + 1) :
j, f (n - j) = jFinset.Ico (n + 1 - m) (n + 1 - k), f j
theorem Finset.prod_range_reflect {M : Type u_2} [] (f : M) (n : ) :
j, f (n - 1 - j) = j, f j
theorem Finset.sum_range_reflect {δ : Type u_3} [] (f : δ) (n : ) :
j, f (n - 1 - j) = j, f j
@[simp]
theorem Finset.prod_Ico_id_eq_factorial (n : ) :
xFinset.Ico 1 (n + 1), x = n.factorial
@[simp]
theorem Finset.prod_range_add_one_eq_factorial (n : ) :
x, (x + 1) = n.factorial
theorem Finset.sum_range_id_mul_two (n : ) :
(∑ i, i) * 2 = n * (n - 1)

Gauss' summation formula

theorem Finset.sum_range_id (n : ) :
i, i = n * (n - 1) / 2

Gauss' summation formula

theorem Finset.sum_range_diag_flip {M : Type u_2} [] (n : ) (f : M) :
m, kFinset.range (m + 1), f k (m - k) = m, kFinset.range (n - m), f m k
theorem Finset.prod_range_diag_flip {M : Type u_2} [] (n : ) (f : M) :
m, kFinset.range (m + 1), f k (m - k) = m, kFinset.range (n - m), f m k
theorem Finset.sum_range_succ_sub_sum {M : Type u_3} (f : M) {n : } [] :
iFinset.range (n + 1), f i - i, f i = f n
theorem Finset.prod_range_succ_div_prod {M : Type u_3} (f : M) {n : } [] :
(∏ iFinset.range (n + 1), f i) / i, f i = f n
theorem Finset.sum_range_succ_sub_top {M : Type u_3} (f : M) {n : } [] :
iFinset.range (n + 1), f i - f n = i, f i
theorem Finset.prod_range_succ_div_top {M : Type u_3} (f : M) {n : } [] :
(∏ iFinset.range (n + 1), f i) / f n = i, f i
theorem Finset.sum_Ico_sub_bot {M : Type u_3} (f : M) {m : } {n : } [] (hmn : m < n) :
i, f i - f m = iFinset.Ico (m + 1) n, f i
theorem Finset.prod_Ico_div_bot {M : Type u_3} (f : M) {m : } {n : } [] (hmn : m < n) :
(∏ i, f i) / f m = iFinset.Ico (m + 1) n, f i
theorem Finset.sum_Ico_succ_sub_top {M : Type u_3} (f : M) {m : } {n : } [] (hmn : m n) :
iFinset.Ico m (n + 1), f i - f n = i, f i
theorem Finset.prod_Ico_succ_div_top {M : Type u_3} (f : M) {m : } {n : } [] (hmn : m n) :
(∏ iFinset.Ico m (n + 1), f i) / f n = i, f i