Big operators indexed by intervals

This file proves lemmas about ∏ x ∈ Ixx a b, f x and ∑ x ∈ Ixx a b, f x.

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

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

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

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

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

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

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

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

theorem Finset.mul_prod_Ioo_eq_prod_Ico {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) : f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x

theorem Finset.add_sum_Ioo_eq_sum_Ico {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) : f a + ∑ x ∈ Ioo a b, f x = ∑ x ∈ Ico a b, f x

theorem Finset.prod_Ioo_mul_eq_prod_Ico {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) : (∏ x ∈ Ioo a b, f x) * f a = ∏ x ∈ Ico a b, f x

theorem Finset.sum_Ioo_add_eq_sum_Ico {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) : ∑ x ∈ Ioo a b, f x + f a = ∑ x ∈ Ico a b, f x

theorem Finset.mul_prod_Ioo_eq_prod_Ioc {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) : f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x

theorem Finset.add_sum_Ioo_eq_sum_Ioc {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) : f b + ∑ x ∈ Ioo a b, f x = ∑ x ∈ Ioc a b, f x

theorem Finset.prod_Ioo_mul_eq_prod_Ioc {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) : (∏ x ∈ Ioo a b, f x) * f b = ∏ x ∈ Ioc a b, f x

theorem Finset.sum_Ioo_add_eq_sum_Ioc {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} {a b : α} [PartialOrder α] [LocallyFiniteOrder α] (h : a < b) : ∑ x ∈ Ioo a b, f x + f b = ∑ x ∈ Ioc a b, f x

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

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

theorem Finset.mul_prod_Ioi_eq_prod_Ici {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) : f a * ∏ x > a, f x = ∏ x ≥ a, f x

theorem Finset.add_sum_Ioi_eq_sum_Ici {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) : f a + ∑ x > a, f x = ∑ x ≥ a, f x

theorem Finset.prod_Ioi_mul_eq_prod_Ici {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) : (∏ x > a, f x) * f a = ∏ x ≥ a, f x

theorem Finset.sum_Ioi_add_eq_sum_Ici {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) : ∑ x > a, f x + f a = ∑ x ≥ a, f x

theorem Finset.mul_prod_Iio_eq_prod_Iic {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) : f a * ∏ x < a, f x = ∏ x ≤ a, f x

theorem Finset.add_sum_Iio_eq_sum_Iic {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) : f a + ∑ x < a, f x = ∑ x ≤ a, f x

theorem Finset.prod_Iio_mul_eq_prod_Iic {α : Type u_1} {M : Type u_2} [CommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) : (∏ x < a, f x) * f a = ∏ x ≤ a, f x

theorem Finset.sum_Iio_add_eq_sum_Iic {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {f : α → M} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) : ∑ x < a, f x + f a = ∑ x ≤ a, f x

theorem Finset.prod_Ico_mul_eq_prod_Ico_add_one {α : Type u_1} {M : Type u_2} [CommMonoid M] {a b : α} [LinearOrder α] [LocallyFiniteOrder α] [AddMonoidWithOne α] [SuccAddOrder α] [NoMaxOrder α] (hab : a ≤ b) (f : α → M) : (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Ico a (b + 1), f x

theorem Finset.sum_Ico_add_eq_sum_Ico_add_one {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {a b : α} [LinearOrder α] [LocallyFiniteOrder α] [AddMonoidWithOne α] [SuccAddOrder α] [NoMaxOrder α] (hab : a ≤ b) (f : α → M) : ∑ x ∈ Ico a b, f x + f b = ∑ x ∈ Ico a (b + 1), f x

theorem Finset.prod_Iio_add_one_comm {α : Type u_1} {M : Type u_2} [CommMonoid M] [LinearOrder α] [LocallyFiniteOrderBot α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M) : ∏ i < a + 1, f i = f a * ∏ i < a, f i

theorem Finset.sum_Iio_add_zero_comm {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [LinearOrder α] [LocallyFiniteOrderBot α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M) : ∑ i < a + 1, f i = f a + ∑ i < a, f i

@[simp]

theorem Finset.prod_Iio_add_one {α : Type u_1} {M : Type u_2} [CommMonoid M] [LinearOrder α] [LocallyFiniteOrderBot α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M) : ∏ i < a + 1, f i = (∏ i < a, f i) * f a

@[simp]

theorem Finset.sum_Iio_add_zero {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [LinearOrder α] [LocallyFiniteOrderBot α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M) : ∑ i < a + 1, f i = ∑ i < a, f i + f a

theorem Finset.prod_Iic_add_one_comm {α : Type u_1} {M : Type u_2} [CommMonoid M] [LinearOrder α] [LocallyFiniteOrderBot α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M) : ∏ i ≤ a + 1, f i = f (a + 1) * ∏ i ≤ a, f i

theorem Finset.sum_Iic_add_zero_comm {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [LinearOrder α] [LocallyFiniteOrderBot α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M) : ∑ i ≤ a + 1, f i = f (a + 1) + ∑ i ≤ a, f i

@[simp]

theorem Finset.prod_Iic_add_one {α : Type u_1} {M : Type u_2} [CommMonoid M] [LinearOrder α] [LocallyFiniteOrderBot α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M) : ∏ i ≤ a + 1, f i = (∏ i ≤ a, f i) * f (a + 1)

@[simp]

theorem Finset.sum_Iic_add_zero {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [LinearOrder α] [LocallyFiniteOrderBot α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M) : ∑ i ≤ a + 1, f i = ∑ i ≤ a, f i + f (a + 1)

theorem Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag {α : Type u_1} {M : Type u_2} [CommMonoid M] [LinearOrder α] [Fintype α] [LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α] (f : α → α → M) : ∏ i : α, ∏ j > i, f j i * f i j = ∏ i : α, ∏ j ∈ {i}ᶜ, f j i

theorem Finset.sum_sum_Ioi_add_eq_sum_sum_off_diag {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [LinearOrder α] [Fintype α] [LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α] (f : α → α → M) : ∑ i : α, ∑ j > i, (f j i + f i j) = ∑ i : α, ∑ j ∈ {i}ᶜ, f j i

theorem Finset.prod_eq_prod_range_sdiff {α : Type u_3} {β : Type u_4} [DecidableEq α] [CommMonoid β] (s : ℕ → Finset α) (hs : Monotone s) (g : α → β) (n : ℕ) : ∏ i ∈ s n, g i = (∏ i ∈ s 0, g i) * ∏ i ∈ range n, ∏ j ∈ s (i + 1) \ s i, g j

Given a sequence of finite sets s₀ ⊆ s₁ ⊆ s₂ ⋯, the product of gᵢ over i ∈ sₙ is equal to ∏_{i ∈ s₀} gᵢ * ∏_{j < n, i ∈ sⱼ₊₁ \ sⱼ} gᵢ.

theorem Finset.sum_eq_sum_range_sdiff {α : Type u_3} {β : Type u_4} [DecidableEq α] [AddCommMonoid β] (s : ℕ → Finset α) (hs : Monotone s) (g : α → β) (n : ℕ) : ∑ i ∈ s n, g i = ∑ i ∈ s 0, g i + ∑ i ∈ range n, ∑ j ∈ s (i + 1) \ s i, g j

Given a sequence of finite sets s₀ ⊆ s₁ ⊆ s₂ ⋯, the sum of gᵢ over i ∈ sₙ is equal to ∑_{i ∈ s₀} gᵢ + ∑_{j < n, i ∈ sⱼ₊₁ \ sⱼ} gᵢ.