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.left_add_sum_Ioc
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[AddCommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a ≤ b)
:
f a + ∑ x ∈ Finset.Ioc a b, f x = ∑ x ∈ Finset.Icc a b, f x
theorem
Finset.left_mul_prod_Ioc
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[CommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a ≤ b)
:
f a * ∏ x ∈ Finset.Ioc a b, f x = ∏ x ∈ Finset.Icc a b, f x
theorem
Finset.sum_Ioc_add_left
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[AddCommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a ≤ b)
:
∑ x ∈ Finset.Ioc a b, f x + f a = ∑ x ∈ Finset.Icc a b, f x
theorem
Finset.prod_Ioc_mul_left
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[CommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a ≤ b)
:
(∏ x ∈ Finset.Ioc a b, f x) * f a = ∏ x ∈ Finset.Icc a b, f x
theorem
Finset.right_add_sum_Ico
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[AddCommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a ≤ b)
:
f b + ∑ x ∈ Finset.Ico a b, f x = ∑ x ∈ Finset.Icc a b, f x
theorem
Finset.right_mul_prod_Ico
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[CommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a ≤ b)
:
f b * ∏ x ∈ Finset.Ico a b, f x = ∏ x ∈ Finset.Icc a b, f x
theorem
Finset.sum_Ico_add_right
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[AddCommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a ≤ b)
:
∑ x ∈ Finset.Ico a b, f x + f b = ∑ x ∈ Finset.Icc a b, f x
theorem
Finset.prod_Ico_mul_right
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[CommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a ≤ b)
:
(∏ x ∈ Finset.Ico a b, f x) * f b = ∏ x ∈ Finset.Icc a b, f x
theorem
Finset.left_add_sum_Ioo
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[AddCommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a < b)
:
f a + ∑ x ∈ Finset.Ioo a b, f x = ∑ x ∈ Finset.Ico a b, f x
theorem
Finset.left_mul_prod_Ioo
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[CommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a < b)
:
f a * ∏ x ∈ Finset.Ioo a b, f x = ∏ x ∈ Finset.Ico a b, f x
theorem
Finset.sum_Ioo_add_left
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[AddCommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a < b)
:
∑ x ∈ Finset.Ioo a b, f x + f a = ∑ x ∈ Finset.Ico a b, f x
theorem
Finset.prod_Ioo_mul_left
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[CommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a < b)
:
(∏ x ∈ Finset.Ioo a b, f x) * f a = ∏ x ∈ Finset.Ico a b, f x
theorem
Finset.right_add_sum_Ioo
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[AddCommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a < b)
:
f b + ∑ x ∈ Finset.Ioo a b, f x = ∑ x ∈ Finset.Ioc a b, f x
theorem
Finset.right_mul_prod_Ioo
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[CommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a < b)
:
f b * ∏ x ∈ Finset.Ioo a b, f x = ∏ x ∈ Finset.Ioc a b, f x
theorem
Finset.sum_Ioo_add_right
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[AddCommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a < b)
:
∑ x ∈ Finset.Ioo a b, f x + f b = ∑ x ∈ Finset.Ioc a b, f x
theorem
Finset.prod_Ioo_mul_right
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[CommMonoid β]
{f : α → β}
{a : α}
{b : α}
[LocallyFiniteOrder α]
(h : a < b)
:
(∏ x ∈ Finset.Ioo a b, f x) * f b = ∏ x ∈ Finset.Ioc a b, f x
theorem
Finset.left_add_sum_Ioi
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[AddCommMonoid β]
{f : α → β}
[LocallyFiniteOrderTop α]
(a : α)
:
f a + ∑ x ∈ Finset.Ioi a, f x = ∑ x ∈ Finset.Ici a, f x
theorem
Finset.left_mul_prod_Ioi
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[CommMonoid β]
{f : α → β}
[LocallyFiniteOrderTop α]
(a : α)
:
f a * ∏ x ∈ Finset.Ioi a, f x = ∏ x ∈ Finset.Ici a, f x
theorem
Finset.sum_Ioi_add_left
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[AddCommMonoid β]
{f : α → β}
[LocallyFiniteOrderTop α]
(a : α)
:
∑ x ∈ Finset.Ioi a, f x + f a = ∑ x ∈ Finset.Ici a, f x
theorem
Finset.prod_Ioi_mul_left
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[CommMonoid β]
{f : α → β}
[LocallyFiniteOrderTop α]
(a : α)
:
(∏ x ∈ Finset.Ioi a, f x) * f a = ∏ x ∈ Finset.Ici a, f x
theorem
Finset.right_add_sum_Iio
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[AddCommMonoid β]
{f : α → β}
[LocallyFiniteOrderBot α]
(a : α)
:
f a + ∑ x ∈ Finset.Iio a, f x = ∑ x ∈ Finset.Iic a, f x
theorem
Finset.right_mul_prod_Iio
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[CommMonoid β]
{f : α → β}
[LocallyFiniteOrderBot α]
(a : α)
:
f a * ∏ x ∈ Finset.Iio a, f x = ∏ x ∈ Finset.Iic a, f x
theorem
Finset.sum_Iio_add_right
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[AddCommMonoid β]
{f : α → β}
[LocallyFiniteOrderBot α]
(a : α)
:
∑ x ∈ Finset.Iio a, f x + f a = ∑ x ∈ Finset.Iic a, f x
theorem
Finset.prod_Iio_mul_right
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[CommMonoid β]
{f : α → β}
[LocallyFiniteOrderBot α]
(a : α)
:
(∏ x ∈ Finset.Iio a, f x) * f a = ∏ x ∈ Finset.Iic a, f x