mathlib3 documentation

data.fintype.big_operators

Results about "big operations" over a fintype, and consequent results about cardinalities of certain types.

Implementation note #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This content had previously been in data.fintype.basic, but was moved here to avoid requiring algebra.big_operators (and hence many other imports) as a dependency of fintype.

However many of the results here really belong in algebra.big_operators.basic and should be moved at some point.

theorem fintype.prod_bool {α : Type u_1} [comm_monoid α] (f : bool α) :
finset.univ.prod (λ (b : bool), f b) = f bool.tt * f bool.ff
theorem fintype.sum_bool {α : Type u_1} [add_comm_monoid α] (f : bool α) :
finset.univ.sum (λ (b : bool), f b) = f bool.tt + f bool.ff
theorem fintype.card_eq_sum_ones {α : Type u_1} [fintype α] :
fintype.card α = finset.univ.sum (λ (a : α), 1)
theorem fintype.prod_extend_by_one {α : Type u_1} {ι : Type u_4} [decidable_eq ι] [fintype ι] [comm_monoid α] (s : finset ι) (f : ι α) :
finset.univ.prod (λ (i : ι), ite (i s) (f i) 1) = s.prod (λ (i : ι), f i)
theorem fintype.sum_extend_by_zero {α : Type u_1} {ι : Type u_4} [decidable_eq ι] [fintype ι] [add_comm_monoid α] (s : finset ι) (f : ι α) :
finset.univ.sum (λ (i : ι), ite (i s) (f i) 0) = s.sum (λ (i : ι), f i)
theorem fintype.prod_eq_one {α : Type u_1} {M : Type u_4} [fintype α] [comm_monoid M] (f : α M) (h : (a : α), f a = 1) :
finset.univ.prod (λ (a : α), f a) = 1
theorem fintype.sum_eq_zero {α : Type u_1} {M : Type u_4} [fintype α] [add_comm_monoid M] (f : α M) (h : (a : α), f a = 0) :
finset.univ.sum (λ (a : α), f a) = 0
theorem fintype.prod_congr {α : Type u_1} {M : Type u_4} [fintype α] [comm_monoid M] (f g : α M) (h : (a : α), f a = g a) :
finset.univ.prod (λ (a : α), f a) = finset.univ.prod (λ (a : α), g a)
theorem fintype.sum_congr {α : Type u_1} {M : Type u_4} [fintype α] [add_comm_monoid M] (f g : α M) (h : (a : α), f a = g a) :
finset.univ.sum (λ (a : α), f a) = finset.univ.sum (λ (a : α), g a)
theorem fintype.prod_eq_single {α : Type u_1} {M : Type u_4} [fintype α] [comm_monoid M] {f : α M} (a : α) (h : (x : α), x a f x = 1) :
finset.univ.prod (λ (x : α), f x) = f a
theorem fintype.sum_eq_single {α : Type u_1} {M : Type u_4} [fintype α] [add_comm_monoid M] {f : α M} (a : α) (h : (x : α), x a f x = 0) :
finset.univ.sum (λ (x : α), f x) = f a
theorem fintype.prod_eq_mul {α : Type u_1} {M : Type u_4} [fintype α] [comm_monoid M] {f : α M} (a b : α) (h₁ : a b) (h₂ : (x : α), x a x b f x = 1) :
finset.univ.prod (λ (x : α), f x) = f a * f b
theorem fintype.sum_eq_add {α : Type u_1} {M : Type u_4} [fintype α] [add_comm_monoid M] {f : α M} (a b : α) (h₁ : a b) (h₂ : (x : α), x a x b f x = 0) :
finset.univ.sum (λ (x : α), f x) = f a + f b
theorem fintype.eq_of_subsingleton_of_prod_eq {M : Type u_4} [comm_monoid M] {ι : Type u_1} [subsingleton ι] {s : finset ι} {f : ι M} {b : M} (h : s.prod (λ (i : ι), f i) = b) (i : ι) (H : i s) :
f i = b

If a product of a finset of a subsingleton type has a given value, so do the terms in that product.

theorem fintype.eq_of_subsingleton_of_sum_eq {M : Type u_4} [add_comm_monoid M] {ι : Type u_1} [subsingleton ι] {s : finset ι} {f : ι M} {b : M} (h : s.sum (λ (i : ι), f i) = b) (i : ι) (H : i s) :
f i = b

If a sum of a finset of a subsingleton type has a given value, so do the terms in that sum.

@[simp]
theorem fintype.prod_option {α : Type u_1} {M : Type u_4} [fintype α] [comm_monoid M] (f : option α M) :
finset.univ.prod (λ (i : option α), f i) = f option.none * finset.univ.prod (λ (i : α), f (option.some i))
@[simp]
theorem fintype.sum_option {α : Type u_1} {M : Type u_4} [fintype α] [add_comm_monoid M] (f : option α M) :
finset.univ.sum (λ (i : option α), f i) = f option.none + finset.univ.sum (λ (i : α), f (option.some i))
@[simp]
theorem fintype.card_sigma {α : Type u_1} (β : α Type u_2) [fintype α] [Π (a : α), fintype (β a)] :
fintype.card (sigma β) = finset.univ.sum (λ (a : α), fintype.card (β a))
@[simp]
theorem finset.card_pi {α : Type u_1} [decidable_eq α] {δ : α Type u_2} (s : finset α) (t : Π (a : α), finset (δ a)) :
(s.pi t).card = s.prod (λ (a : α), (t a).card)
@[simp]
theorem fintype.card_pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α Type u_2} (t : Π (a : α), finset (δ a)) :
(fintype.pi_finset t).card = finset.univ.prod (λ (a : α), (t a).card)
@[simp]
theorem fintype.card_pi {α : Type u_1} {β : α Type u_2} [decidable_eq α] [fintype α] [f : Π (a : α), fintype (β a)] :
fintype.card (Π (a : α), β a) = finset.univ.prod (λ (a : α), fintype.card (β a))
@[simp]
theorem fintype.card_fun {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] [fintype β] :
@[simp]
theorem card_vector {α : Type u_1} [fintype α] (n : ) :
@[simp]
theorem finset.prod_attach_univ {α : Type u_1} {β : Type u_2} [fintype α] [comm_monoid β] (f : {a // a finset.univ} β) :
finset.univ.attach.prod (λ (x : {x // x finset.univ}), f x) = finset.univ.prod (λ (x : α), f x, _⟩)
@[simp]
theorem finset.sum_attach_univ {α : Type u_1} {β : Type u_2} [fintype α] [add_comm_monoid β] (f : {a // a finset.univ} β) :
finset.univ.attach.sum (λ (x : {x // x finset.univ}), f x) = finset.univ.sum (λ (x : α), f x, _⟩)
theorem finset.prod_univ_pi {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] [comm_monoid β] {δ : α Type u_3} {t : Π (a : α), finset (δ a)} (f : (Π (a : α), a finset.univ δ a) β) :
(finset.univ.pi t).prod (λ (x : Π (a : α), a finset.univ δ a), f x) = (fintype.pi_finset t).prod (λ (x : Π (a : α), δ a), f (λ (a : α) (_x : a finset.univ), x a))

Taking a product over univ.pi t is the same as taking the product over fintype.pi_finset t. univ.pi t and fintype.pi_finset t are essentially the same finset, but differ in the type of their element, univ.pi t is a finset (Π a ∈ univ, t a) and fintype.pi_finset t is a finset (Π a, t a).

theorem finset.sum_univ_pi {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] [add_comm_monoid β] {δ : α Type u_3} {t : Π (a : α), finset (δ a)} (f : (Π (a : α), a finset.univ δ a) β) :
(finset.univ.pi t).sum (λ (x : Π (a : α), a finset.univ δ a), f x) = (fintype.pi_finset t).sum (λ (x : Π (a : α), δ a), f (λ (a : α) (_x : a finset.univ), x a))

Taking a sum over univ.pi t is the same as taking the sum over fintype.pi_finset t. univ.pi t and fintype.pi_finset t are essentially the same finset, but differ in the type of their element, univ.pi t is a finset (Π a ∈ univ, t a) and fintype.pi_finset t is a finset (Π a, t a).

theorem finset.prod_univ_sum {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] [comm_semiring β] {δ : α Type u_1} [Π (a : α), decidable_eq (δ a)] {t : Π (a : α), finset (δ a)} {f : Π (a : α), δ a β} :
finset.univ.prod (λ (a : α), (t a).sum (λ (b : δ a), f a b)) = (fintype.pi_finset t).sum (λ (p : Π (a : α), δ a), finset.univ.prod (λ (x : α), f x (p x)))

The product over univ of a sum can be written as a sum over the product of sets, fintype.pi_finset. finset.prod_sum is an alternative statement when the product is not over univ

theorem fintype.sum_pow_mul_eq_add_pow (α : Type u_1) [fintype α] {R : Type u_2} [comm_semiring R] (a b : R) :
finset.univ.sum (λ (s : finset α), a ^ s.card * b ^ (fintype.card α - s.card)) = (a + b) ^ fintype.card α

Summing a^s.card * b^(n-s.card) over all finite subsets s of a fintype of cardinality n gives (a + b)^n. The "good" proof involves expanding along all coordinates using the fact that x^n is multilinear, but multilinear maps are only available now over rings, so we give instead a proof reducing to the usual binomial theorem to have a result over semirings.

theorem function.bijective.sum_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [fintype β] [add_comm_monoid γ] {f : α β} (hf : function.bijective f) (g : β γ) :
finset.univ.sum (λ (i : α), g (f i)) = finset.univ.sum (λ (i : β), g i)
theorem function.bijective.prod_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [fintype β] [comm_monoid γ] {f : α β} (hf : function.bijective f) (g : β γ) :
finset.univ.prod (λ (i : α), g (f i)) = finset.univ.prod (λ (i : β), g i)
theorem equiv.sum_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [fintype β] [add_comm_monoid γ] (e : α β) (f : β γ) :
finset.univ.sum (λ (i : α), f (e i)) = finset.univ.sum (λ (i : β), f i)
theorem equiv.prod_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [fintype β] [comm_monoid γ] (e : α β) (f : β γ) :
finset.univ.prod (λ (i : α), f (e i)) = finset.univ.prod (λ (i : β), f i)
theorem equiv.sum_comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [fintype β] [add_comm_monoid γ] (e : α β) (f : α γ) (g : β γ) (h : (i : α), f i = g (e i)) :
finset.univ.sum (λ (i : α), f i) = finset.univ.sum (λ (i : β), g i)
theorem equiv.prod_comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [fintype β] [comm_monoid γ] (e : α β) (f : α γ) (g : β γ) (h : (i : α), f i = g (e i)) :
finset.univ.prod (λ (i : α), f i) = finset.univ.prod (λ (i : β), g i)
theorem fin.sum_univ_eq_sum_range {α : Type u_1} [add_comm_monoid α] (f : α) (n : ) :
finset.univ.sum (λ (i : fin n), f i) = (finset.range n).sum (λ (i : ), f i)

It is equivalent to sum a function over fin n or finset.range n.

theorem fin.prod_univ_eq_prod_range {α : Type u_1} [comm_monoid α] (f : α) (n : ) :
finset.univ.prod (λ (i : fin n), f i) = (finset.range n).prod (λ (i : ), f i)

It is equivalent to compute the product of a function over fin n or finset.range n.

theorem finset.prod_fin_eq_prod_range {β : Type u_2} [comm_monoid β] {n : } (c : fin n β) :
finset.univ.prod (λ (i : fin n), c i) = (finset.range n).prod (λ (i : ), dite (i < n) (λ (h : i < n), c i, h⟩) (λ (h : ¬i < n), 1))
theorem finset.sum_fin_eq_sum_range {β : Type u_2} [add_comm_monoid β] {n : } (c : fin n β) :
finset.univ.sum (λ (i : fin n), c i) = (finset.range n).sum (λ (i : ), dite (i < n) (λ (h : i < n), c i, h⟩) (λ (h : ¬i < n), 0))
theorem finset.sum_to_finset_eq_subtype {α : Type u_1} {M : Type u_2} [add_comm_monoid M] [fintype α] (p : α Prop) [decidable_pred p] (f : α M) :
{x : α | p x}.to_finset.sum (λ (a : α), f a) = finset.univ.sum (λ (a : subtype p), f a)
theorem finset.prod_to_finset_eq_subtype {α : Type u_1} {M : Type u_2} [comm_monoid M] [fintype α] (p : α Prop) [decidable_pred p] (f : α M) :
{x : α | p x}.to_finset.prod (λ (a : α), f a) = finset.univ.prod (λ (a : subtype p), f a)
theorem finset.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] [fintype β] [comm_monoid γ] (s : finset α) (f : α β) (g : α γ) :
finset.univ.prod (λ (b : β), (finset.filter (λ (a : α), f a = b) s).prod (λ (a : α), g a)) = s.prod (λ (a : α), g a)
theorem finset.sum_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] [fintype β] [add_comm_monoid γ] (s : finset α) (f : α β) (g : α γ) :
finset.univ.sum (λ (b : β), (finset.filter (λ (a : α), f a = b) s).sum (λ (a : α), g a)) = s.sum (λ (a : α), g a)
theorem fintype.sum_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [decidable_eq β] [fintype β] [add_comm_monoid γ] (f : α β) (g : α γ) :
finset.univ.sum (λ (b : β), finset.univ.sum (λ (a : {a // f a = b}), g a)) = finset.univ.sum (λ (a : α), g a)
theorem fintype.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [decidable_eq β] [fintype β] [comm_monoid γ] (f : α β) (g : α γ) :
finset.univ.prod (λ (b : β), finset.univ.prod (λ (a : {a // f a = b}), g a)) = finset.univ.prod (λ (a : α), g a)
theorem fintype.prod_dite {α : Type u_1} {β : Type u_2} [fintype α] {p : α Prop} [decidable_pred p] [comm_monoid β] (f : Π (a : α), p a β) (g : Π (a : α), ¬p a β) :
finset.univ.prod (λ (a : α), dite (p a) (f a) (g a)) = finset.univ.prod (λ (a : {a // p a}), f a _) * finset.univ.prod (λ (a : {a // ¬p a}), g a _)
theorem fintype.prod_sum_elim {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [fintype α₁] [fintype α₂] [comm_monoid M] (f : α₁ M) (g : α₂ M) :
finset.univ.prod (λ (x : α₁ α₂), sum.elim f g x) = finset.univ.prod (λ (a₁ : α₁), f a₁) * finset.univ.prod (λ (a₂ : α₂), g a₂)
theorem fintype.sum_sum_elim {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [fintype α₁] [fintype α₂] [add_comm_monoid M] (f : α₁ M) (g : α₂ M) :
finset.univ.sum (λ (x : α₁ α₂), sum.elim f g x) = finset.univ.sum (λ (a₁ : α₁), f a₁) + finset.univ.sum (λ (a₂ : α₂), g a₂)
@[simp]
theorem fintype.sum_sum_type {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [fintype α₁] [fintype α₂] [add_comm_monoid M] (f : α₁ α₂ M) :
finset.univ.sum (λ (x : α₁ α₂), f x) = finset.univ.sum (λ (a₁ : α₁), f (sum.inl a₁)) + finset.univ.sum (λ (a₂ : α₂), f (sum.inr a₂))
@[simp]
theorem fintype.prod_sum_type {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [fintype α₁] [fintype α₂] [comm_monoid M] (f : α₁ α₂ M) :
finset.univ.prod (λ (x : α₁ α₂), f x) = finset.univ.prod (λ (a₁ : α₁), f (sum.inl a₁)) * finset.univ.prod (λ (a₂ : α₂), f (sum.inr a₂))