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.Ico a b).sum fun (x : α) => f x) = (Finset.Icc a b).sum 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.Ico a b).prod fun (x : α) => f x) = (Finset.Icc a b).prod 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.Ico a b).sum fun (x : α) => f x) + f b = (Finset.Icc a b).sum 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.Ico a b).prod fun (x : α) => f x) * f b = (Finset.Icc a b).prod 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.Ioc a b).sum fun (x : α) => f x) = (Finset.Icc a b).sum 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.Ioc a b).prod fun (x : α) => f x) = (Finset.Icc a b).prod 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.Ioc a b).sum fun (x : α) => f x) + f a = (Finset.Icc a b).sum 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.Ioc a b).prod fun (x : α) => f x) * f a = (Finset.Icc a b).prod 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.Ioi a).sum fun (x : α) => f x) = (Finset.Ici a).sum 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.Ioi a).prod fun (x : α) => f x) = (Finset.Ici a).prod 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.Ioi a).sum fun (x : α) => f x) + f a = (Finset.Ici a).sum 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.Ioi a).prod fun (x : α) => f x) * f a = (Finset.Ici a).prod 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.Iio a).sum fun (x : α) => f x) = (Finset.Iic a).sum 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.Iio a).prod fun (x : α) => f x) = (Finset.Iic a).prod 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.Iio a).sum fun (x : α) => f x) + f a = (Finset.Iic a).sum 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.Iio a).prod fun (x : α) => f x) * f a = (Finset.Iic a).prod fun (x : α) => f x
theorem
Finset.sum_sum_Ioi_add_eq_sum_sum_off_diag
{α : Type u_1}
{M : Type u_2}
[Fintype α]
[LinearOrder α]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot α]
[AddCommMonoid M]
(f : α → α → M)
:
(Finset.univ.sum fun (i : α) => (Finset.Ioi i).sum fun (j : α) => f j i + f i j) = Finset.univ.sum fun (i : α) => {i}ᶜ.sum fun (j : α) => f j i
theorem
Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag
{α : Type u_1}
{M : Type u_2}
[Fintype α]
[LinearOrder α]
[LocallyFiniteOrderTop α]
[LocallyFiniteOrderBot α]
[CommMonoid M]
(f : α → α → M)
:
(Finset.univ.prod fun (i : α) => (Finset.Ioi i).prod fun (j : α) => f j i * f i j) = Finset.univ.prod fun (i : α) => {i}ᶜ.prod fun (j : α) => f j i
theorem
Finset.sum_Ico_add'
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[OrderedCancelAddCommMonoid α]
[ExistsAddOfLE α]
[LocallyFiniteOrder α]
(f : α → M)
(a : α)
(b : α)
(c : α)
:
((Finset.Ico a b).sum fun (x : α) => f (x + c)) = (Finset.Ico (a + c) (b + c)).sum 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.Ico a b).prod fun (x : α) => f (x + c)) = (Finset.Ico (a + c) (b + c)).prod 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.Ico a b).sum fun (x : α) => f (c + x)) = (Finset.Ico (a + c) (b + c)).sum 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.Ico a b).prod fun (x : α) => f (c + x)) = (Finset.Ico (a + c) (b + c)).prod fun (x : α) => f x
theorem
Finset.sum_Ico_succ_top
{M : Type u_2}
[AddCommMonoid M]
{a : ℕ}
{b : ℕ}
(hab : a ≤ b)
(f : ℕ → M)
:
((Finset.Ico a (b + 1)).sum fun (k : ℕ) => f k) = ((Finset.Ico a b).sum 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.Ico a (b + 1)).prod fun (k : ℕ) => f k) = ((Finset.Ico a b).prod 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.Ico a b).sum fun (k : ℕ) => f k) = f a + (Finset.Ico (a + 1) b).sum 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.Ico a b).prod fun (k : ℕ) => f k) = f a * (Finset.Ico (a + 1) b).prod 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.Ico m n).sum fun (i : ℕ) => f i) + (Finset.Ico n k).sum fun (i : ℕ) => f i) = (Finset.Ico m k).sum 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.Ico m n).prod fun (i : ℕ) => f i) * (Finset.Ico n k).prod fun (i : ℕ) => f i) = (Finset.Ico m k).prod 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.Ioc m n).sum fun (i : ℕ) => f i) + (Finset.Ioc n k).sum fun (i : ℕ) => f i) = (Finset.Ioc m k).sum 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.Ioc m n).prod fun (i : ℕ) => f i) * (Finset.Ioc n k).prod fun (i : ℕ) => f i) = (Finset.Ioc m k).prod fun (i : ℕ) => f i
theorem
Finset.sum_Ioc_succ_top
{M : Type u_2}
[AddCommMonoid M]
{a : ℕ}
{b : ℕ}
(hab : a ≤ b)
(f : ℕ → M)
:
((Finset.Ioc a (b + 1)).sum fun (k : ℕ) => f k) = ((Finset.Ioc a b).sum 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.Ioc a (b + 1)).prod fun (k : ℕ) => f k) = ((Finset.Ioc a b).prod 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.range m).sum fun (k : ℕ) => f k) + (Finset.Ico m n).sum fun (k : ℕ) => f k) = (Finset.range n).sum 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.range m).prod fun (k : ℕ) => f k) * (Finset.Ico m n).prod fun (k : ℕ) => f k) = (Finset.range n).prod fun (k : ℕ) => f k
theorem
Finset.sum_Ico_eq_add_neg
{δ : Type u_3}
[AddCommGroup δ]
(f : ℕ → δ)
{m : ℕ}
{n : ℕ}
(h : m ≤ n)
:
((Finset.Ico m n).sum fun (k : ℕ) => f k) = ((Finset.range n).sum fun (k : ℕ) => f k) + -(Finset.range m).sum fun (k : ℕ) => f k
theorem
Finset.prod_Ico_eq_mul_inv
{δ : Type u_3}
[CommGroup δ]
(f : ℕ → δ)
{m : ℕ}
{n : ℕ}
(h : m ≤ n)
:
((Finset.Ico m n).prod fun (k : ℕ) => f k) = ((Finset.range n).prod fun (k : ℕ) => f k) * ((Finset.range m).prod fun (k : ℕ) => f k)⁻¹
theorem
Finset.sum_Ico_eq_sub
{δ : Type u_3}
[AddCommGroup δ]
(f : ℕ → δ)
{m : ℕ}
{n : ℕ}
(h : m ≤ n)
:
((Finset.Ico m n).sum fun (k : ℕ) => f k) = ((Finset.range n).sum fun (k : ℕ) => f k) - (Finset.range m).sum fun (k : ℕ) => f k
theorem
Finset.prod_Ico_eq_div
{δ : Type u_3}
[CommGroup δ]
(f : ℕ → δ)
{m : ℕ}
{n : ℕ}
(h : m ≤ n)
:
((Finset.Ico m n).prod fun (k : ℕ) => f k) = ((Finset.range n).prod fun (k : ℕ) => f k) / (Finset.range m).prod fun (k : ℕ) => f k
theorem
Finset.sum_range_sub_sum_range
{α : Type u_3}
[AddCommGroup α]
{f : ℕ → α}
{n : ℕ}
{m : ℕ}
(hnm : n ≤ m)
:
(((Finset.range m).sum fun (k : ℕ) => f k) - (Finset.range n).sum fun (k : ℕ) => f k) = (Finset.filter (fun (k : ℕ) => n ≤ k) (Finset.range m)).sum fun (k : ℕ) => f k
theorem
Finset.prod_range_div_prod_range
{α : Type u_3}
[CommGroup α]
{f : ℕ → α}
{n : ℕ}
{m : ℕ}
(hnm : n ≤ m)
:
(((Finset.range m).prod fun (k : ℕ) => f k) / (Finset.range n).prod fun (k : ℕ) => f k) = (Finset.filter (fun (k : ℕ) => n ≤ k) (Finset.range m)).prod fun (k : ℕ) => f k
theorem
Finset.sum_Ico_Ico_comm
{M : Type u_3}
[AddCommMonoid M]
(a : ℕ)
(b : ℕ)
(f : ℕ → ℕ → M)
:
((Finset.Ico a b).sum fun (i : ℕ) => (Finset.Ico i b).sum fun (j : ℕ) => f i j) = (Finset.Ico a b).sum fun (j : ℕ) => (Finset.Ico a (j + 1)).sum 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_Ico_comm'
{M : Type u_3}
[AddCommMonoid M]
(a : ℕ)
(b : ℕ)
(f : ℕ → ℕ → M)
:
((Finset.Ico a b).sum fun (i : ℕ) => (Finset.Ico (i + 1) b).sum fun (j : ℕ) => f i j) = (Finset.Ico a b).sum fun (j : ℕ) => (Finset.Ico a j).sum 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.Ico m n).sum fun (k : ℕ) => f k) = (Finset.range (n - m)).sum fun (k : ℕ) => f (m + k)
theorem
Finset.prod_Ico_eq_prod_range
{M : Type u_2}
[CommMonoid M]
(f : ℕ → M)
(m : ℕ)
(n : ℕ)
:
((Finset.Ico m n).prod fun (k : ℕ) => f k) = (Finset.range (n - m)).prod 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.Ico k m).prod fun (j : ℕ) => f (n - j)) = (Finset.Ico (n + 1 - m) (n + 1 - k)).prod fun (j : ℕ) => f j
theorem
Finset.sum_Ico_reflect
{δ : Type u_3}
[AddCommMonoid δ]
(f : ℕ → δ)
(k : ℕ)
{m : ℕ}
{n : ℕ}
(h : m ≤ n + 1)
:
((Finset.Ico k m).sum fun (j : ℕ) => f (n - j)) = (Finset.Ico (n + 1 - m) (n + 1 - k)).sum fun (j : ℕ) => f j
theorem
Finset.prod_range_reflect
{M : Type u_2}
[CommMonoid M]
(f : ℕ → M)
(n : ℕ)
:
((Finset.range n).prod fun (j : ℕ) => f (n - 1 - j)) = (Finset.range n).prod fun (j : ℕ) => f j
theorem
Finset.sum_range_reflect
{δ : Type u_3}
[AddCommMonoid δ]
(f : ℕ → δ)
(n : ℕ)
:
((Finset.range n).sum fun (j : ℕ) => f (n - 1 - j)) = (Finset.range n).sum fun (j : ℕ) => f j
@[simp]
theorem
Finset.prod_Ico_id_eq_factorial
(n : ℕ)
:
((Finset.Ico 1 (n + 1)).prod fun (x : ℕ) => x) = n.factorial
@[simp]
theorem
Finset.prod_range_add_one_eq_factorial
(n : ℕ)
:
((Finset.range n).prod fun (x : ℕ) => x + 1) = n.factorial
Gauss' summation formula
Gauss' summation formula
theorem
Finset.sum_range_diag_flip
{M : Type u_2}
[AddCommMonoid M]
(n : ℕ)
(f : ℕ → ℕ → M)
:
((Finset.range n).sum fun (m : ℕ) => (Finset.range (m + 1)).sum fun (k : ℕ) => f k (m - k)) = (Finset.range n).sum fun (m : ℕ) => (Finset.range (n - m)).sum fun (k : ℕ) => f m k
theorem
Finset.prod_range_diag_flip
{M : Type u_2}
[CommMonoid M]
(n : ℕ)
(f : ℕ → ℕ → M)
:
((Finset.range n).prod fun (m : ℕ) => (Finset.range (m + 1)).prod fun (k : ℕ) => f k (m - k)) = (Finset.range n).prod fun (m : ℕ) => (Finset.range (n - m)).prod fun (k : ℕ) => f m k
theorem
Finset.sum_range_succ_sub_sum
{M : Type u_3}
(f : ℕ → M)
{n : ℕ}
[AddCommGroup M]
:
(((Finset.range (n + 1)).sum fun (i : ℕ) => f i) - (Finset.range n).sum fun (i : ℕ) => f i) = f n
theorem
Finset.prod_range_succ_div_prod
{M : Type u_3}
(f : ℕ → M)
{n : ℕ}
[CommGroup M]
:
(((Finset.range (n + 1)).prod fun (i : ℕ) => f i) / (Finset.range n).prod fun (i : ℕ) => f i) = f n
theorem
Finset.sum_range_succ_sub_top
{M : Type u_3}
(f : ℕ → M)
{n : ℕ}
[AddCommGroup M]
:
((Finset.range (n + 1)).sum fun (i : ℕ) => f i) - f n = (Finset.range n).sum fun (i : ℕ) => f i
theorem
Finset.prod_range_succ_div_top
{M : Type u_3}
(f : ℕ → M)
{n : ℕ}
[CommGroup M]
:
((Finset.range (n + 1)).prod fun (i : ℕ) => f i) / f n = (Finset.range n).prod fun (i : ℕ) => f i
theorem
Finset.sum_Ico_sub_bot
{M : Type u_3}
(f : ℕ → M)
{m : ℕ}
{n : ℕ}
[AddCommGroup M]
(hmn : m < n)
:
((Finset.Ico m n).sum fun (i : ℕ) => f i) - f m = (Finset.Ico (m + 1) n).sum fun (i : ℕ) => f i
theorem
Finset.prod_Ico_div_bot
{M : Type u_3}
(f : ℕ → M)
{m : ℕ}
{n : ℕ}
[CommGroup M]
(hmn : m < n)
:
((Finset.Ico m n).prod fun (i : ℕ) => f i) / f m = (Finset.Ico (m + 1) n).prod 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.Ico m (n + 1)).sum fun (i : ℕ) => f i) - f n = (Finset.Ico m n).sum 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.Ico m (n + 1)).prod fun (i : ℕ) => f i) / f n = (Finset.Ico m n).prod fun (i : ℕ) => f i