mathlib documentation

algebra.big_operators.fin

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.

source
theorem finset.sum_range {β : Type u_2} [add_comm_monoid β] {n : ℕ} (f : ℕ → β) :
∑ (i : ℕ) in finset.range n, f i = ∑ (i : fin n), f ↑i
source
theorem finset.prod_range {β : Type u_2} [comm_monoid β] {n : ℕ} (f : ℕ → β) :
∏ (i : ℕ) in finset.range n, f i = ∏ (i : fin n), f ↑i
source
theorem fin.prod_univ_def {β : Type u_2} [comm_monoid β] {n : ℕ} (f : fin n → β) :
∏ (i : fin n), f i = (list.map f (list.fin_range n)).prod
source
theorem fin.sum_univ_def {β : Type u_2} [add_comm_monoid β] {n : ℕ} (f : fin n → β) :
∑ (i : fin n), f i = (list.map f (list.fin_range n)).sum
source
theorem fin.sum_of_fn {β : Type u_2} [add_comm_monoid β] {n : ℕ} (f : fin n → β) :
(list.of_fn f).sum = ∑ (i : fin n), f i
source
theorem fin.prod_of_fn {β : Type u_2} [comm_monoid β] {n : ℕ} (f : fin n → β) :
(list.of_fn f).prod = ∏ (i : fin n), f i
source
theorem fin.sum_univ_zero {β : Type u_2} [add_comm_monoid β] (f : fin 0 → β) :
∑ (i : fin 0), f i = 0

A sum of a function f : fin 0 → β is 0 because fin 0 is empty

source
theorem fin.prod_univ_zero {β : Type u_2} [comm_monoid β] (f : fin 0 → β) :
∏ (i : fin 0), f i = 1

A product of a function f : fin 0 → β is 1 because fin 0 is empty

source
theorem fin.prod_univ_succ_above {β : Type u_2} [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) (x : fin (n + 1)) :
∏ (i : fin (n + 1)), f i = (f x) * ∏ (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

source
theorem fin.sum_univ_succ_above {β : Type u_2} [add_comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) (x : fin (n + 1)) :
∑ (i : fin (n + 1)), f i = f x + ∑ (i : fin n), f (⇑(x.succ_above) i)
source
theorem fin.prod_univ_succ {β : Type u_2} [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
∏ (i : fin (n + 1)), f i = (f 0) * ∏ (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

source
theorem fin.sum_univ_succ {β : Type u_2} [add_comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
∑ (i : fin (n + 1)), f i = f 0 + ∑ (i : fin n), f i.succ
source
theorem fin.sum_univ_cast_succ {β : Type u_2} [add_comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
∑ (i : fin (n + 1)), f i = ∑ (i : fin n), f (⇑fin.cast_succ i) + f (fin.last n)
source
theorem fin.prod_univ_cast_succ {β : Type u_2} [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
∏ (i : fin (n + 1)), f i = (∏ (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

source
theorem fin.prod_univ_one {β : Type u_2} [comm_monoid β] (f : fin 1 → β) :
∏ (i : fin 1), f i = f 0
source
theorem fin.sum_univ_one {β : Type u_2} [add_comm_monoid β] (f : fin 1 → β) :
∑ (i : fin 1), f i = f 0
source
theorem fin.prod_univ_two {β : Type u_2} [comm_monoid β] (f : fin 2 → β) :
∏ (i : fin 2), f i = (f 0) * f 1
source
theorem fin.sum_univ_two {β : Type u_2} [add_comm_monoid β] (f : fin 2 → β) :
∑ (i : fin 2), f i = f 0 + f 1
source
theorem fin.sum_pow_mul_eq_add_pow {n : ℕ} {R : Type u_1} [comm_semiring R] (a b : R) :
∑ (s : finset (fin n)), (a ^ s.card) * b ^ (n - s.card) = (a + b) ^ n
source
theorem fin.prod_const {α : Type u_1} [comm_monoid α] (n : ℕ) (x : α) :
∏ (i : fin n), x = x ^ n
source
theorem fin.sum_const {α : Type u_1} [add_comm_monoid α] (n : ℕ) (x : α) :
∑ (i : fin n), x = n • x
source
theorem fin.sum_filter_zero_lt {M : Type u_1} [add_comm_monoid M] {n : ℕ} {v : fin n.succ → M} :
∑ (i : fin n.succ) in finset.filter (λ (i : fin n.succ), 0 < i) finset.univ, v i = ∑ (j : fin n), v j.succ
source
theorem fin.prod_filter_zero_lt {M : Type u_1} [comm_monoid M] {n : ℕ} {v : fin n.succ → M} :
∏ (i : fin n.succ) in finset.filter (λ (i : fin n.succ), 0 < i) finset.univ, v i = ∏ (j : fin n), v j.succ
source
theorem fin.prod_filter_succ_lt {M : Type u_1} [comm_monoid M] {n : ℕ} (j : fin n) (v : fin n.succ → M) :
∏ (i : fin n.succ) in finset.filter (λ (i : fin n.succ), j.succ < i) finset.univ, v i = ∏ (j : fin n) in finset.filter (λ (i : fin n), j < i) finset.univ, v j.succ
source
theorem fin.sum_filter_succ_lt {M : Type u_1} [add_comm_monoid M] {n : ℕ} (j : fin n) (v : fin n.succ → M) :
∑ (i : fin n.succ) in finset.filter (λ (i : fin n.succ), j.succ < i) finset.univ, v i = ∑ (j : fin n) in finset.filter (λ (i : fin n), j < i) finset.univ, v j.succ
source
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 = ∑ (j : fin n) in finset.filter (λ (j : fin n), j.val < i) finset.univ, f j
source
theorem list.prod_take_of_fn {α : Type u_1} [comm_monoid α] {n : ℕ} (f : fin n → α) (i : ℕ) :
(list.take i (list.of_fn f)).prod = ∏ (j : fin n) in finset.filter (λ (j : fin n), j.val < i) finset.univ, f j
source
theorem list.sum_of_fn {α : Type u_1} [add_comm_monoid α] {n : ℕ} {f : fin n → α} :
(list.of_fn f).sum = ∑ (i : fin n), f i
source
theorem list.prod_of_fn {α : Type u_1} [comm_monoid α] {n : ℕ} {f : fin n → α} :
(list.of_fn f).prod = ∏ (i : fin n), f i
source
theorem list.alternating_sum_eq_finset_sum {G : Type u_1} [add_comm_group G] (L : list G) :
L.alternating_sum = ∑ (i : fin L.length), (-1) ^ ↑i • L.nth_le ↑i _
source
theorem list.alternating_prod_eq_finset_prod {G : Type u_1} [comm_group G] (L : list G) :
L.alternating_prod = ∏ (i : fin L.length), L.nth_le ↑i _ ^ (-1) ^ ↑i