Results about big operators over intervals

We prove results about big operators over intervals.

theorem Finset.prod_Ico_add' {α : Type u_1} {M : Type u_3} [CommMonoid M] [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (f : α → M) (a b c : α) : ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico (a + c) (b + c), f x

theorem Finset.sum_Ico_add' {α : Type u_1} {M : Type u_3} [AddCommMonoid M] [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (f : α → M) (a b c : α) : ∑ x ∈ Ico a b, f (x + c) = ∑ x ∈ Ico (a + c) (b + c), f x

theorem Finset.prod_Ico_add {α : Type u_1} {M : Type u_3} [CommMonoid M] [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (f : α → M) (a b c : α) : ∏ x ∈ Ico a b, f (c + x) = ∏ x ∈ Ico (a + c) (b + c), f x

theorem Finset.sum_Ico_add {α : Type u_1} {M : Type u_3} [AddCommMonoid M] [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (f : α → M) (a b c : α) : ∑ x ∈ Ico a b, f (c + x) = ∑ x ∈ Ico (a + c) (b + c), f x

@[simp]

theorem Finset.prod_Ico_add_right_sub_eq {α : Type u_1} {M : Type u_3} [CommMonoid M] {f : α → M} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [Sub α] [OrderedSub α] (a b c : α) : ∏ x ∈ Ico (a + c) (b + c), f (x - c) = ∏ x ∈ Ico a b, f x

@[simp]

theorem Finset.sum_Ico_add_right_sub_eq {α : Type u_1} {M : Type u_3} [AddCommMonoid M] {f : α → M} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [Sub α] [OrderedSub α] (a b c : α) : ∑ x ∈ Ico (a + c) (b + c), f (x - c) = ∑ x ∈ Ico a b, f x

theorem Finset.prod_Ico_succ_top {M : Type u_3} [CommMonoid M] {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) : ∏ k ∈ Ico a (b + 1), f k = (∏ k ∈ Ico a b, f k) * f b

theorem Finset.sum_Ico_succ_top {M : Type u_3} [AddCommMonoid M] {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) : ∑ k ∈ Ico a (b + 1), f k = ∑ k ∈ Ico a b, f k + f b

theorem Finset.prod_Ico_consecutive {M : Type u_3} [CommMonoid M] (f : ℕ → M) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : (∏ i ∈ Ico m n, f i) * ∏ i ∈ Ico n k, f i = ∏ i ∈ Ico m k, f i

theorem Finset.sum_Ico_consecutive {M : Type u_3} [AddCommMonoid M] (f : ℕ → M) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : ∑ i ∈ Ico m n, f i + ∑ i ∈ Ico n k, f i = ∑ i ∈ Ico m k, f i

theorem Finset.prod_Ioc_consecutive {M : Type u_3} [CommMonoid M] (f : ℕ → M) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : (∏ i ∈ Ioc m n, f i) * ∏ i ∈ Ioc n k, f i = ∏ i ∈ Ioc m k, f i

theorem Finset.sum_Ioc_consecutive {M : Type u_3} [AddCommMonoid M] (f : ℕ → M) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : ∑ i ∈ Ioc m n, f i + ∑ i ∈ Ioc n k, f i = ∑ i ∈ Ioc m k, f i

theorem Finset.prod_Ioc_succ_top {M : Type u_3} [CommMonoid M] {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) : ∏ k ∈ Ioc a (b + 1), f k = (∏ k ∈ Ioc a b, f k) * f (b + 1)

theorem Finset.sum_Ioc_succ_top {M : Type u_3} [AddCommMonoid M] {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) : ∑ k ∈ Ioc a (b + 1), f k = ∑ k ∈ Ioc a b, f k + f (b + 1)

theorem Finset.prod_Icc_succ_top {M : Type u_3} [CommMonoid M] {a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) : ∏ k ∈ Icc a (b + 1), f k = (∏ k ∈ Icc a b, f k) * f (b + 1)

theorem Finset.sum_Icc_succ_top {M : Type u_3} [AddCommMonoid M] {a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) : ∑ k ∈ Icc a (b + 1), f k = ∑ k ∈ Icc a b, f k + f (b + 1)

theorem Finset.prod_range_mul_prod_Ico {M : Type u_3} [CommMonoid M] (f : ℕ → M) {m n : ℕ} (h : m ≤ n) : (∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k = ∏ k ∈ range n, f k

theorem Finset.sum_range_add_sum_Ico {M : Type u_3} [AddCommMonoid M] (f : ℕ → M) {m n : ℕ} (h : m ≤ n) : ∑ k ∈ range m, f k + ∑ k ∈ Ico m n, f k = ∑ k ∈ range n, f k

theorem Finset.prod_range_eq_mul_Ico {M : Type u_3} [CommMonoid M] (f : ℕ → M) {n : ℕ} (hn : 0 < n) : ∏ x ∈ range n, f x = f 0 * ∏ x ∈ Ico 1 n, f x

theorem Finset.sum_range_eq_add_Ico {M : Type u_3} [AddCommMonoid M] (f : ℕ → M) {n : ℕ} (hn : 0 < n) : ∑ x ∈ range n, f x = f 0 + ∑ x ∈ Ico 1 n, f x

theorem Finset.prod_Ico_eq_mul_inv {δ : Type u_4} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) : ∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) * (∏ k ∈ range m, f k)⁻¹

theorem Finset.sum_Ico_eq_add_neg {δ : Type u_4} [AddCommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) : ∑ k ∈ Ico m n, f k = ∑ k ∈ range n, f k + -∑ k ∈ range m, f k

theorem Finset.prod_Ico_eq_div {δ : Type u_4} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) : ∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) / ∏ k ∈ range m, f k

theorem Finset.sum_Ico_eq_sub {δ : Type u_4} [AddCommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) : ∑ k ∈ Ico m n, f k = ∑ k ∈ range n, f k - ∑ k ∈ range m, f k

theorem Finset.prod_range_div_prod_range {G : Type u_4} [CommGroup G] {f : ℕ → G} {n m : ℕ} (hnm : n ≤ m) : (∏ k ∈ range m, f k) / ∏ k ∈ range n, f k = ∏ k ∈ range m with n ≤ k, f k

theorem Finset.sum_range_sub_sum_range {G : Type u_4} [AddCommGroup G] {f : ℕ → G} {n m : ℕ} (hnm : n ≤ m) : ∑ k ∈ range m, f k - ∑ k ∈ range n, f k = ∑ k ∈ range m with n ≤ k, f k

theorem Finset.sum_Ico_Ico_comm {M : Type u_4} [AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M) : ∑ i ∈ Ico a b, ∑ j ∈ Ico i b, f i j = ∑ j ∈ Ico a b, ∑ i ∈ 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_4} [AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M) : ∑ i ∈ Ico a b, ∑ j ∈ Ico (i + 1) b, f i j = ∑ j ∈ Ico a b, ∑ i ∈ Ico a j, f i j

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

theorem Finset.prod_Ico_eq_prod_range {M : Type u_3} [CommMonoid M] (f : ℕ → M) (m n : ℕ) : ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

theorem Finset.sum_Ico_eq_sum_range {M : Type u_3} [AddCommMonoid M] (f : ℕ → M) (m n : ℕ) : ∑ k ∈ Ico m n, f k = ∑ k ∈ range (n - m), f (m + k)

theorem Finset.prod_Ico_reflect {M : Type u_3} [CommMonoid M] (f : ℕ → M) (k : ℕ) {m n : ℕ} (h : m ≤ n + 1) : ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j

theorem Finset.sum_Ico_reflect {δ : Type u_4} [AddCommMonoid δ] (f : ℕ → δ) (k : ℕ) {m n : ℕ} (h : m ≤ n + 1) : ∑ j ∈ Ico k m, f (n - j) = ∑ j ∈ Ico (n + 1 - m) (n + 1 - k), f j

theorem Finset.prod_range_reflect {M : Type u_3} [CommMonoid M] (f : ℕ → M) (n : ℕ) : ∏ j ∈ range n, f (n - 1 - j) = ∏ j ∈ range n, f j

theorem Finset.sum_range_reflect {δ : Type u_4} [AddCommMonoid δ] (f : ℕ → δ) (n : ℕ) : ∑ j ∈ range n, f (n - 1 - j) = ∑ j ∈ range n, f j

@[simp]

theorem Finset.prod_Ico_id_eq_factorial (n : ℕ) : ∏ x ∈ Ico 1 (n + 1), x = n.factorial

theorem Finset.sum_range_id_mul_two (n : ℕ) : (∑ i ∈ range n, i) * 2 = n * (n - 1)

Gauss' summation formula

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

Gauss' summation formula

theorem Finset.prod_range_diag_flip {M : Type u_3} [CommMonoid M] (n : ℕ) (f : ℕ → ℕ → M) : ∏ m ∈ range n, ∏ k ∈ range (m + 1), f k (m - k) = ∏ m ∈ range n, ∏ k ∈ range (n - m), f m k

theorem Finset.sum_range_diag_flip {M : Type u_3} [AddCommMonoid M] (n : ℕ) (f : ℕ → ℕ → M) : ∑ m ∈ range n, ∑ k ∈ range (m + 1), f k (m - k) = ∑ m ∈ range n, ∑ k ∈ range (n - m), f m k

theorem Finset.prod_range_succ_div_prod {M : Type u_4} (f : ℕ → M) {n : ℕ} [CommGroup M] : (∏ i ∈ range (n + 1), f i) / ∏ i ∈ range n, f i = f n

theorem Finset.sum_range_succ_sub_sum {M : Type u_4} (f : ℕ → M) {n : ℕ} [AddCommGroup M] : ∑ i ∈ range (n + 1), f i - ∑ i ∈ range n, f i = f n

theorem Finset.prod_range_succ_div_top {M : Type u_4} (f : ℕ → M) {n : ℕ} [CommGroup M] : (∏ i ∈ range (n + 1), f i) / f n = ∏ i ∈ range n, f i

theorem Finset.sum_range_succ_sub_top {M : Type u_4} (f : ℕ → M) {n : ℕ} [AddCommGroup M] : ∑ i ∈ range (n + 1), f i - f n = ∑ i ∈ range n, f i

theorem Finset.prod_Ico_div_bot {M : Type u_4} (f : ℕ → M) {m n : ℕ} [CommGroup M] (hmn : m < n) : (∏ i ∈ Ico m n, f i) / f m = ∏ i ∈ Ico (m + 1) n, f i

theorem Finset.sum_Ico_sub_bot {M : Type u_4} (f : ℕ → M) {m n : ℕ} [AddCommGroup M] (hmn : m < n) : ∑ i ∈ Ico m n, f i - f m = ∑ i ∈ Ico (m + 1) n, f i

theorem Finset.prod_Ico_succ_div_top {M : Type u_4} (f : ℕ → M) {m n : ℕ} [CommGroup M] (hmn : m ≤ n) : (∏ i ∈ Ico m (n + 1), f i) / f n = ∏ i ∈ Ico m n, f i

theorem Finset.sum_Ico_succ_sub_top {M : Type u_4} (f : ℕ → M) {m n : ℕ} [AddCommGroup M] (hmn : m ≤ n) : ∑ i ∈ Ico m (n + 1), f i - f n = ∑ i ∈ Ico m n, f i

theorem Finset.prod_Ico_div {M : Type u_4} (f : ℕ → M) {m n : ℕ} [CommGroup M] (hmn : m ≤ n) : ∏ i ∈ Ico m n, f (i + 1) / f i = f n / f m

theorem Finset.sum_Ico_sub {M : Type u_4} (f : ℕ → M) {m n : ℕ} [AddCommGroup M] (hmn : m ≤ n) : ∑ i ∈ Ico m n, (f (i + 1) - f i) = f n - f m

theorem Finset.prod_Icc_div {M : Type u_4} {m n : ℕ} [CommGroup M] (hmn : m ≤ n) (f : ℕ → M) : ∏ i ∈ Icc m n, f (i + 1) / f i = f (n + 1) / f m

theorem Finset.sum_Icc_sub {M : Type u_4} {m n : ℕ} [AddCommGroup M] (hmn : m ≤ n) (f : ℕ → M) : ∑ i ∈ Icc m n, (f (i + 1) - f i) = f (n + 1) - f m

theorem Finset.prod_fin_Icc_eq_prod_nat_Icc {α : Type u_1} [CommMonoid α] {n : ℕ} (a b : Fin n) (f : Fin n → α) : ∏ i ∈ Icc a b, f i = ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1

theorem Finset.sum_fin_Icc_eq_sum_nat_Icc {α : Type u_1} [AddCommMonoid α] {n : ℕ} (a b : Fin n) (f : Fin n → α) : ∑ i ∈ Icc a b, f i = ∑ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 0

theorem Fin.prod_Iic_div {M : Type u_3} [CommGroup M] {n : ℕ} (a : Fin n) (f : Fin (n + 1) → M) : ∏ i ∈ Finset.Iic a, f i.succ / f i.castSucc = f a.succ / f 0

Telescopic product over Fin.

theorem Fin.sum_Iic_sub {M : Type u_3} [AddCommGroup M] {n : ℕ} (a : Fin n) (f : Fin (n + 1) → M) : ∑ i ∈ Finset.Iic a, (f i.succ - f i.castSucc) = f a.succ - f 0

Telescopic sum over Fin.

theorem Fin.prod_Icc_div {M : Type u_3} [CommGroup M] {n : ℕ} {a b : Fin n} (hab : a ≤ b) (f : Fin (n + 1) → M) : ∏ i ∈ Finset.Icc a b, f i.succ / f i.castSucc = f b.succ / f a.castSucc

Telescopic product over Fin.

theorem Fin.sum_Icc_sub {M : Type u_3} [AddCommGroup M] {n : ℕ} {a b : Fin n} (hab : a ≤ b) (f : Fin (n + 1) → M) : ∑ i ∈ Finset.Icc a b, (f i.succ - f i.castSucc) = f b.succ - f a.castSucc

Telescopic sum over Fin.