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.

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.sum_pow_mul_eq_add_pow {n : } {R : Type u_1} [comm_semiring R] (a b : R) :
finset.univ.sum (λ (s : finset (fin n)), a ^ s.card * b ^ (n - s.card)) = (a + b) ^ n
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)
theorem list.alternating_sum_eq_finset_sum {G : Type u_1} [add_comm_group G] (L : list G) :
L.alternating_sum = finset.univ.sum (λ (i : fin L.length), (-1) ^ i L.nth_le i _)
theorem list.alternating_prod_eq_finset_prod {G : Type u_1} [comm_group G] (L : list G) :
L.alternating_prod = finset.univ.prod (λ (i : fin L.length), L.nth_le i _ ^ (-1) ^ i)