Results about big operators over intervals #

We prove results about big operators over intervals (mostly the ℕ-valued Ico m n).

theorem Finset.sum_Ico_add' {α : Type u} {β : Type v} [inst : AddCommMonoid β] [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (f : α → β) (a : α) (b : α) (c : α) :

(Finset.sum (Finset.Ico a b) fun x => f (x + c)) = Finset.sum (Finset.Ico (a + c) (b + c)) fun x => f x

source

ink

theorem Finset.prod_Ico_add' {α : Type u} {β : Type v} [inst : CommMonoid β] [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (f : α → β) (a : α) (b : α) (c : α) :

(Finset.prod (Finset.Ico a b) fun x => f (x + c)) = Finset.prod (Finset.Ico (a + c) (b + c)) fun x => f x

source

ink

theorem Finset.sum_Ico_add {α : Type u} {β : Type v} [inst : AddCommMonoid β] [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (f : α → β) (a : α) (b : α) (c : α) :

(Finset.sum (Finset.Ico a b) fun x => f (c + x)) = Finset.sum (Finset.Ico (a + c) (b + c)) fun x => f x

source

ink

theorem Finset.prod_Ico_add {α : Type u} {β : Type v} [inst : CommMonoid β] [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (f : α → β) (a : α) (b : α) (c : α) :

(Finset.prod (Finset.Ico a b) fun x => f (c + x)) = Finset.prod (Finset.Ico (a + c) (b + c)) fun x => f x

source

ink

theorem Finset.sum_Ico_succ_top {β : Type v} [inst : AddCommMonoid β] {a : ℕ} {b : ℕ} (hab : a ≤ b) (f : ℕ → β) :

(Finset.sum (Finset.Ico a (b + 1)) fun k => f k) = (Finset.sum (Finset.Ico a b) fun k => f k) + f b

source

ink

theorem Finset.prod_Ico_succ_top {β : Type v} [inst : CommMonoid β] {a : ℕ} {b : ℕ} (hab : a ≤ b) (f : ℕ → β) :

(Finset.prod (Finset.Ico a (b + 1)) fun k => f k) = (Finset.prod (Finset.Ico a b) fun k => f k) * f b

source

ink

theorem Finset.sum_eq_sum_Ico_succ_bot {β : Type v} [inst : AddCommMonoid β] {a : ℕ} {b : ℕ} (hab : a < b) (f : ℕ → β) :

(Finset.sum (Finset.Ico a b) fun k => f k) = f a + Finset.sum (Finset.Ico (a + 1) b) fun k => f k

source

ink

theorem Finset.prod_eq_prod_Ico_succ_bot {β : Type v} [inst : CommMonoid β] {a : ℕ} {b : ℕ} (hab : a < b) (f : ℕ → β) :

(Finset.prod (Finset.Ico a b) fun k => f k) = f a * Finset.prod (Finset.Ico (a + 1) b) fun k => f k

source

ink

theorem Finset.sum_Ico_consecutive {β : Type v} [inst : AddCommMonoid β] (f : ℕ → β) {m : ℕ} {n : ℕ} {k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) :

((Finset.sum (Finset.Ico m n) fun i => f i) + Finset.sum (Finset.Ico n k) fun i => f i) = Finset.sum (Finset.Ico m k) fun i => f i

source

ink

theorem Finset.prod_Ico_consecutive {β : Type v} [inst : CommMonoid β] (f : ℕ → β) {m : ℕ} {n : ℕ} {k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) :

((Finset.prod (Finset.Ico m n) fun i => f i) * Finset.prod (Finset.Ico n k) fun i => f i) = Finset.prod (Finset.Ico m k) fun i => f i

source

ink

theorem Finset.sum_Ioc_consecutive {β : Type v} [inst : AddCommMonoid β] (f : ℕ → β) {m : ℕ} {n : ℕ} {k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) :

((Finset.sum (Finset.Ioc m n) fun i => f i) + Finset.sum (Finset.Ioc n k) fun i => f i) = Finset.sum (Finset.Ioc m k) fun i => f i

source

ink

theorem Finset.prod_Ioc_consecutive {β : Type v} [inst : CommMonoid β] (f : ℕ → β) {m : ℕ} {n : ℕ} {k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) :

((Finset.prod (Finset.Ioc m n) fun i => f i) * Finset.prod (Finset.Ioc n k) fun i => f i) = Finset.prod (Finset.Ioc m k) fun i => f i

source

ink

theorem Finset.sum_Ioc_succ_top {β : Type v} [inst : AddCommMonoid β] {a : ℕ} {b : ℕ} (hab : a ≤ b) (f : ℕ → β) :

(Finset.sum (Finset.Ioc a (b + 1)) fun k => f k) = (Finset.sum (Finset.Ioc a b) fun k => f k) + f (b + 1)

source

ink

theorem Finset.prod_Ioc_succ_top {β : Type v} [inst : CommMonoid β] {a : ℕ} {b : ℕ} (hab : a ≤ b) (f : ℕ → β) :

(Finset.prod (Finset.Ioc a (b + 1)) fun k => f k) = (Finset.prod (Finset.Ioc a b) fun k => f k) * f (b + 1)

source

ink

theorem Finset.sum_range_add_sum_Ico {β : Type v} [inst : AddCommMonoid β] (f : ℕ → β) {m : ℕ} {n : ℕ} (h : m ≤ n) :

((Finset.sum (Finset.range m) fun k => f k) + Finset.sum (Finset.Ico m n) fun k => f k) = Finset.sum (Finset.range n) fun k => f k

source

ink

theorem Finset.prod_range_mul_prod_Ico {β : Type v} [inst : CommMonoid β] (f : ℕ → β) {m : ℕ} {n : ℕ} (h : m ≤ n) :

((Finset.prod (Finset.range m) fun k => f k) * Finset.prod (Finset.Ico m n) fun k => f k) = Finset.prod (Finset.range n) fun k => f k

source

ink

theorem Finset.sum_Ico_eq_add_neg {δ : Type u_1} [inst : AddCommGroup δ] (f : ℕ → δ) {m : ℕ} {n : ℕ} (h : m ≤ n) :

(Finset.sum (Finset.Ico m n) fun k => f k) = (Finset.sum (Finset.range n) fun k => f k) + -Finset.sum (Finset.range m) fun k => f k

source

ink

theorem Finset.prod_Ico_eq_mul_inv {δ : Type u_1} [inst : CommGroup δ] (f : ℕ → δ) {m : ℕ} {n : ℕ} (h : m ≤ n) :

(Finset.prod (Finset.Ico m n) fun k => f k) = (Finset.prod (Finset.range n) fun k => f k) * (Finset.prod (Finset.range m) fun k => f k)⁻¹

source

ink

theorem Finset.sum_Ico_eq_sub {δ : Type u_1} [inst : AddCommGroup δ] (f : ℕ → δ) {m : ℕ} {n : ℕ} (h : m ≤ n) :

(Finset.sum (Finset.Ico m n) fun k => f k) = (Finset.sum (Finset.range n) fun k => f k) - Finset.sum (Finset.range m) fun k => f k

source

ink

theorem Finset.prod_Ico_eq_div {δ : Type u_1} [inst : CommGroup δ] (f : ℕ → δ) {m : ℕ} {n : ℕ} (h : m ≤ n) :

(Finset.prod (Finset.Ico m n) fun k => f k) = (Finset.prod (Finset.range n) fun k => f k) / Finset.prod (Finset.range m) fun k => f k

source

ink

theorem Finset.sum_range_sub_sum_range {α : Type u_1} [inst : AddCommGroup α] {f : ℕ → α} {n : ℕ} {m : ℕ} (hnm : n ≤ m) :

((Finset.sum (Finset.range m) fun k => f k) - Finset.sum (Finset.range n) fun k => f k) = Finset.sum (Finset.filter (fun k => n ≤ k) (Finset.range m)) fun k => f k

source

ink

theorem Finset.prod_range_sub_prod_range {α : Type u_1} [inst : CommGroup α] {f : ℕ → α} {n : ℕ} {m : ℕ} (hnm : n ≤ m) :

((Finset.prod (Finset.range m) fun k => f k) / Finset.prod (Finset.range n) fun k => f k) = Finset.prod (Finset.filter (fun k => n ≤ k) (Finset.range m)) fun k => f k

source

ink

theorem Finset.sum_Ico_Ico_comm {M : Type u_1} [inst : AddCommMonoid M] (a : ℕ) (b : ℕ) (f : ℕ → ℕ → M) :

(Finset.sum (Finset.Ico a b) fun i => Finset.sum (Finset.Ico i b) fun j => f i j) = Finset.sum (Finset.Ico a b) fun j => Finset.sum (Finset.Ico a (j + 1)) fun i => f i j

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

source

ink

theorem
Finset.sum_Ico_eq_sum_range
{β : Type v}

[inst : AddCommMonoid β]

(f : ℕ → β)

(m : ℕ)

(n : ℕ)
 :(Finset.sum (Finset.Ico m n) fun k => f k) = Finset.sum (Finset.range (n - m)) fun k => f (m + k)

source

ink

theorem
Finset.prod_Ico_eq_prod_range
{β : Type v}

[inst : CommMonoid β]

(f : ℕ → β)

(m : ℕ)

(n : ℕ)
 :(Finset.prod (Finset.Ico m n) fun k => f k) = Finset.prod (Finset.range (n - m)) fun k => f (m + k)

source

ink

theorem
Finset.prod_Ico_reflect
{β : Type v}

[inst : CommMonoid β]

(f : ℕ → β)

(k : ℕ)

{m : ℕ}

{n : ℕ}

(h : m ≤ n + 1)
 :(Finset.prod (Finset.Ico k m) fun j => f (n - j)) = Finset.prod (Finset.Ico (n + 1 - m) (n + 1 - k)) fun j => f j

source

ink

theorem
Finset.sum_Ico_reflect
{δ : Type u_1}

[inst : AddCommMonoid δ]

(f : ℕ → δ)

(k : ℕ)

{m : ℕ}

{n : ℕ}

(h : m ≤ n + 1)
 :(Finset.sum (Finset.Ico k m) fun j => f (n - j)) = Finset.sum (Finset.Ico (n + 1 - m) (n + 1 - k)) fun j => f j

source

ink

theorem
Finset.prod_range_reflect
{β : Type v}

[inst : CommMonoid β]

(f : ℕ → β)

(n : ℕ)
 :(Finset.prod (Finset.range n) fun j => f (n - 1 - j)) = Finset.prod (Finset.range n) fun j => f j

source

ink

theorem
Finset.sum_range_reflect
{δ : Type u_1}

[inst : AddCommMonoid δ]

(f : ℕ → δ)

(n : ℕ)
 :(Finset.sum (Finset.range n) fun j => f (n - 1 - j)) = Finset.sum (Finset.range n) fun j => f j

source

ink

@[simp]


theorem
Finset.prod_Ico_id_eq_factorial
(n : ℕ)
 :(Finset.prod (Finset.Ico 1 (n + 1)) fun x => x) = Nat.factorial n

source

ink

@[simp]


theorem
Finset.prod_range_add_one_eq_factorial
(n : ℕ)
 :(Finset.prod (Finset.range n) fun x => x + 1) = Nat.factorial n

source

ink

theorem
Finset.sum_range_id_mul_two
(n : ℕ)
 :(Finset.sum (Finset.range n) fun i => i) * 2 = n * (n - 1)

Gauss' summation formula

source

ink

theorem
Finset.sum_range_id
(n : ℕ)
 :(Finset.sum (Finset.range n) fun i => i) = n * (n - 1) / 2

Gauss' summation formula

source

ink

theorem
Finset.sum_range_succ_sub_sum
{β : Type u_1}

(f : ℕ → β)

{n : ℕ}

[inst : AddCommGroup β]
 :((Finset.sum (Finset.range (n + 1)) fun i => f i) - Finset.sum (Finset.range n) fun i => f i) = f n

source

ink

theorem
Finset.prod_range_succ_div_prod
{β : Type u_1}

(f : ℕ → β)

{n : ℕ}

[inst : CommGroup β]
 :((Finset.prod (Finset.range (n + 1)) fun i => f i) / Finset.prod (Finset.range n) fun i => f i) = f n

source

ink

theorem
Finset.sum_range_succ_sub_top
{β : Type u_1}

(f : ℕ → β)

{n : ℕ}

[inst : AddCommGroup β]
 :(Finset.sum (Finset.range (n + 1)) fun i => f i) - f n = Finset.sum (Finset.range n) fun i => f i

source

ink

theorem
Finset.prod_range_succ_div_top
{β : Type u_1}

(f : ℕ → β)

{n : ℕ}

[inst : CommGroup β]
 :(Finset.prod (Finset.range (n + 1)) fun i => f i) / f n = Finset.prod (Finset.range n) fun i => f i

source

ink

theorem
Finset.sum_Ico_sub_bot
{β : Type u_1}

(f : ℕ → β)

{m : ℕ}

{n : ℕ}

[inst : AddCommGroup β]

(hmn : m < n)
 :(Finset.sum (Finset.Ico m n) fun i => f i) - f m = Finset.sum (Finset.Ico (m + 1) n) fun i => f i

source

ink

theorem
Finset.prod_Ico_div_bot
{β : Type u_1}

(f : ℕ → β)

{m : ℕ}

{n : ℕ}

[inst : CommGroup β]

(hmn : m < n)
 :(Finset.prod (Finset.Ico m n) fun i => f i) / f m = Finset.prod (Finset.Ico (m + 1) n) fun i => f i

source

ink

theorem
Finset.sum_Ico_succ_sub_top
{β : Type u_1}

(f : ℕ → β)

{m : ℕ}

{n : ℕ}

[inst : AddCommGroup β]

(hmn : m ≤ n)
 :(Finset.sum (Finset.Ico m (n + 1)) fun i => f i) - f n = Finset.sum (Finset.Ico m n) fun i => f i

source

ink

theorem
Finset.prod_Ico_succ_div_top
{β : Type u_1}

(f : ℕ → β)

{m : ℕ}

{n : ℕ}

[inst : CommGroup β]

(hmn : m ≤ n)
 :(Finset.prod (Finset.Ico m (n + 1)) fun i => f i) / f n = Finset.prod (Finset.Ico m n) fun i => f i

source

ink

theorem
Finset.sum_Ico_by_parts
{R : Type u_2}

{M : Type u_1}

[inst : Ring R]

[inst : AddCommGroup M]

[inst : Module R M]

(f : ℕ → R)

(g : ℕ → M)

{m : ℕ}

{n : ℕ}

(hmn : m < n)
 :(Finset.sum (Finset.Ico m n) fun i => f i • g i) =   ((f (n - 1) • Finset.sum (Finset.range n) fun i => g i) - f m • Finset.sum (Finset.range m) fun i => g i) -     Finset.sum (Finset.Ico m (n - 1)) fun i => (f (i + 1) - f i) • Finset.sum (Finset.range (i + 1)) fun i => g i

Summation by parts, also known as Abel's lemma or an Abel transformation

source

ink

theorem
Finset.sum_range_by_parts
{R : Type u_2}

{M : Type u_1}

[inst : Ring R]

[inst : AddCommGroup M]

[inst : Module R M]

(f : ℕ → R)

(g : ℕ → M)

(n : ℕ)
 :(Finset.sum (Finset.range n) fun i => f i • g i) =   (f (n - 1) • Finset.sum (Finset.range n) fun i => g i) -     Finset.sum (Finset.range (n - 1)) fun i => (f (i + 1) - f i) • Finset.sum (Finset.range (i + 1)) fun i => g i

Summation by parts for ranges