Big operators and fin #
Some results about products and sums over the type fin.
The most important results are the induction formulas fin.prod_univ_cast_succ
and fin.prod_univ_succ, and the formula fin.prod_const for the product of a
constant function. These results have variants for sums instead of products.
theorem
finset.sum_range
{β : Type u_2}
[add_comm_monoid β]
{n : ℕ}
(f : ℕ → β) :
(finset.range n).sum (λ (i : ℕ), f i) = finset.univ.sum (λ (i : fin n), f ↑i)
theorem
finset.prod_range
{β : Type u_2}
[comm_monoid β]
{n : ℕ}
(f : ℕ → β) :
(finset.range n).prod (λ (i : ℕ), f i) = finset.univ.prod (λ (i : fin n), f ↑i)
theorem
fin.prod_univ_def
{β : Type u_2}
[comm_monoid β]
{n : ℕ}
(f : fin n → β) :
finset.univ.prod (λ (i : fin n), f i) = (list.map f (list.fin_range n)).prod
theorem
fin.sum_univ_def
{β : Type u_2}
[add_comm_monoid β]
{n : ℕ}
(f : fin n → β) :
finset.univ.sum (λ (i : fin n), f i) = (list.map f (list.fin_range n)).sum
theorem
fin.sum_of_fn
{β : Type u_2}
[add_comm_monoid β]
{n : ℕ}
(f : fin n → β) :
(list.of_fn f).sum = finset.univ.sum (λ (i : fin n), f i)
theorem
fin.prod_of_fn
{β : Type u_2}
[comm_monoid β]
{n : ℕ}
(f : fin n → β) :
(list.of_fn f).prod = finset.univ.prod (λ (i : fin n), f i)
theorem
fin.sum_univ_zero
{β : Type u_2}
[add_comm_monoid β]
(f : fin 0 → β) :
finset.univ.sum (λ (i : fin 0), f i) = 0
A sum of a function f : fin 0 → β is 0 because fin 0 is empty
theorem
fin.prod_univ_zero
{β : Type u_2}
[comm_monoid β]
(f : fin 0 → β) :
finset.univ.prod (λ (i : fin 0), f i) = 1
A product of a function f : fin 0 → β is 1 because fin 0 is empty
theorem
fin.prod_univ_succ_above
{β : Type u_2}
[comm_monoid β]
{n : ℕ}
(f : fin (n + 1) → β)
(x : fin (n + 1)) :
finset.univ.prod (λ (i : fin (n + 1)), f i) = f x * finset.univ.prod (λ (i : fin n), f (⇑(x.succ_above) i))
A product of a function f : fin (n + 1) → β over all fin (n + 1)
is the product of f x, for some x : fin (n + 1) times the remaining product
theorem
fin.sum_univ_succ_above
{β : Type u_2}
[add_comm_monoid β]
{n : ℕ}
(f : fin (n + 1) → β)
(x : fin (n + 1)) :
finset.univ.sum (λ (i : fin (n + 1)), f i) = f x + finset.univ.sum (λ (i : fin n), f (⇑(x.succ_above) i))
theorem
fin.prod_univ_succ
{β : Type u_2}
[comm_monoid β]
{n : ℕ}
(f : fin (n + 1) → β) :
finset.univ.prod (λ (i : fin (n + 1)), f i) = f 0 * finset.univ.prod (λ (i : fin n), f i.succ)
A product of a function f : fin (n + 1) → β over all fin (n + 1)
is the product of f 0 plus the remaining product
theorem
fin.sum_univ_succ
{β : Type u_2}
[add_comm_monoid β]
{n : ℕ}
(f : fin (n + 1) → β) :
finset.univ.sum (λ (i : fin (n + 1)), f i) = f 0 + finset.univ.sum (λ (i : fin n), f i.succ)
theorem
fin.sum_univ_cast_succ
{β : Type u_2}
[add_comm_monoid β]
{n : ℕ}
(f : fin (n + 1) → β) :
finset.univ.sum (λ (i : fin (n + 1)), f i) = finset.univ.sum (λ (i : fin n), f (⇑fin.cast_succ i)) + f (fin.last n)
theorem
fin.prod_univ_cast_succ
{β : Type u_2}
[comm_monoid β]
{n : ℕ}
(f : fin (n + 1) → β) :
finset.univ.prod (λ (i : fin (n + 1)), f i) = finset.univ.prod (λ (i : fin n), f (⇑fin.cast_succ i)) * f (fin.last n)
A product of a function f : fin (n + 1) → β over all fin (n + 1)
is the product of f (fin.last n) plus the remaining product
theorem
fin.prod_univ_one
{β : Type u_2}
[comm_monoid β]
(f : fin 1 → β) :
finset.univ.prod (λ (i : fin 1), f i) = f 0
theorem
fin.sum_univ_one
{β : Type u_2}
[add_comm_monoid β]
(f : fin 1 → β) :
finset.univ.sum (λ (i : fin 1), f i) = f 0
theorem
fin.prod_univ_two
{β : Type u_2}
[comm_monoid β]
(f : fin 2 → β) :
finset.univ.prod (λ (i : fin 2), f i) = f 0 * f 1
theorem
fin.sum_univ_two
{β : Type u_2}
[add_comm_monoid β]
(f : fin 2 → β) :
finset.univ.sum (λ (i : fin 2), f i) = f 0 + f 1
theorem
fin.prod_const
{α : Type u_1}
[comm_monoid α]
(n : ℕ)
(x : α) :
finset.univ.prod (λ (i : fin n), x) = x ^ n
theorem
fin.sum_const
{α : Type u_1}
[add_comm_monoid α]
(n : ℕ)
(x : α) :
finset.univ.sum (λ (i : fin n), x) = n • x
theorem
fin.sum_filter_zero_lt
{M : Type u_1}
[add_comm_monoid M]
{n : ℕ}
{v : fin n.succ → M} :
(finset.filter (λ (i : fin n.succ), 0 < i) finset.univ).sum (λ (i : fin n.succ), v i) = finset.univ.sum (λ (j : fin n), v j.succ)
theorem
fin.prod_filter_zero_lt
{M : Type u_1}
[comm_monoid M]
{n : ℕ}
{v : fin n.succ → M} :
(finset.filter (λ (i : fin n.succ), 0 < i) finset.univ).prod (λ (i : fin n.succ), v i) = finset.univ.prod (λ (j : fin n), v j.succ)
theorem
fin.prod_filter_succ_lt
{M : Type u_1}
[comm_monoid M]
{n : ℕ}
(j : fin n)
(v : fin n.succ → M) :
(finset.filter (λ (i : fin n.succ), j.succ < i) finset.univ).prod (λ (i : fin n.succ), v i) = (finset.filter (λ (i : fin n), j < i) finset.univ).prod (λ (j : fin n), v j.succ)
theorem
fin.sum_filter_succ_lt
{M : Type u_1}
[add_comm_monoid M]
{n : ℕ}
(j : fin n)
(v : fin n.succ → M) :
(finset.filter (λ (i : fin n.succ), j.succ < i) finset.univ).sum (λ (i : fin n.succ), v i) = (finset.filter (λ (i : fin n), j < i) finset.univ).sum (λ (j : fin n), v j.succ)
theorem
fin.sum_congr'
{M : Type u_1}
[add_comm_monoid M]
{a b : ℕ}
(f : fin b → M)
(h : a = b) :
finset.univ.sum (λ (i : fin a), f (⇑(fin.cast h) i)) = finset.univ.sum (λ (i : fin b), f i)
theorem
fin.prod_congr'
{M : Type u_1}
[comm_monoid M]
{a b : ℕ}
(f : fin b → M)
(h : a = b) :
finset.univ.prod (λ (i : fin a), f (⇑(fin.cast h) i)) = finset.univ.prod (λ (i : fin b), f i)
theorem
fin.prod_univ_add
{M : Type u_1}
[comm_monoid M]
{a b : ℕ}
(f : fin (a + b) → M) :
finset.univ.prod (λ (i : fin (a + b)), f i) = finset.univ.prod (λ (i : fin a), f (⇑(fin.cast_add b) i)) * finset.univ.prod (λ (i : fin b), f (⇑(fin.nat_add a) i))
theorem
fin.sum_univ_add
{M : Type u_1}
[add_comm_monoid M]
{a b : ℕ}
(f : fin (a + b) → M) :
finset.univ.sum (λ (i : fin (a + b)), f i) = finset.univ.sum (λ (i : fin a), f (⇑(fin.cast_add b) i)) + finset.univ.sum (λ (i : fin b), f (⇑(fin.nat_add a) i))
theorem
fin.prod_trunc
{M : Type u_1}
[comm_monoid M]
{a b : ℕ}
(f : fin (a + b) → M)
(hf : ∀ (j : fin b), f (⇑(fin.nat_add a) j) = 1) :
finset.univ.prod (λ (i : fin (a + b)), f i) = finset.univ.prod (λ (i : fin a), f (⇑(fin.cast_le _) i))
theorem
fin.sum_trunc
{M : Type u_1}
[add_comm_monoid M]
{a b : ℕ}
(f : fin (a + b) → M)
(hf : ∀ (j : fin b), f (⇑(fin.nat_add a) j) = 0) :
finset.univ.sum (λ (i : fin (a + b)), f i) = finset.univ.sum (λ (i : fin a), f (⇑(fin.cast_le _) i))
theorem
list.sum_take_of_fn
{α : Type u_1}
[add_comm_monoid α]
{n : ℕ}
(f : fin n → α)
(i : ℕ) :
(list.take i (list.of_fn f)).sum = (finset.filter (λ (j : fin n), j.val < i) finset.univ).sum (λ (j : fin n), f j)
theorem
list.prod_take_of_fn
{α : Type u_1}
[comm_monoid α]
{n : ℕ}
(f : fin n → α)
(i : ℕ) :
(list.take i (list.of_fn f)).prod = (finset.filter (λ (j : fin n), j.val < i) finset.univ).prod (λ (j : fin n), f j)
theorem
list.sum_of_fn
{α : Type u_1}
[add_comm_monoid α]
{n : ℕ}
{f : fin n → α} :
(list.of_fn f).sum = finset.univ.sum (λ (i : fin n), f i)
theorem
list.prod_of_fn
{α : Type u_1}
[comm_monoid α]
{n : ℕ}
{f : fin n → α} :
(list.of_fn f).prod = finset.univ.prod (λ (i : fin n), f i)