Results about "big operations" over a fintype, and consequent
results about cardinalities of certain types.
Implementation note #
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_extend_by_one
{α : Type u_1}
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
[comm_monoid α]
(s : finset ι)
(f : ι → α) :
theorem
fintype.sum_extend_by_zero
{α : Type u_1}
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
[add_comm_monoid α]
(s : finset ι)
(f : ι → α) :
theorem
fintype.prod_eq_one
{α : Type u_1}
{M : Type u_4}
[fintype α]
[comm_monoid M]
(f : α → M)
(h : ∀ (a : α), f a = 1) :
∏ (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) :
∑ (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) :
∏ (a : α), f a = ∏ (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) :
∑ (a : α), f a = ∑ (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) :
∏ (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) :
∑ (x : α), f x = f a
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 : ∏ (i : ι) in s, 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 : ∑ (i : ι) in s, 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) :
@[simp]
theorem
fintype.sum_option
{α : Type u_1}
{M : Type u_4}
[fintype α]
[add_comm_monoid M]
(f : option α → M) :
@[simp]
theorem
fintype.card_sigma
{α : Type u_1}
(β : α → Type u_2)
[fintype α]
[Π (a : α), fintype (β a)] :
fintype.card (sigma β) = ∑ (a : α), fintype.card (β a)
@[simp]
theorem
finset.card_pi
{α : Type u_1}
[decidable_eq α]
{δ : α → Type u_2}
(s : finset α)
(t : Π (a : α), finset (δ a)) :
@[simp]
theorem
fintype.card_pi_finset
{α : Type u_1}
[decidable_eq α]
[fintype α]
{δ : α → Type u_2}
(t : Π (a : α), finset (δ a)) :
(fintype.pi_finset t).card = ∏ (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) = ∏ (a : α), fintype.card (β a)
@[simp]
theorem
fintype.card_fun
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[fintype α]
[fintype β] :
fintype.card (α → β) = fintype.card β ^ fintype.card α
@[simp]
theorem
card_vector
{α : Type u_1}
[fintype α]
(n : ℕ) :
fintype.card (vector α n) = fintype.card α ^ n
@[simp]
theorem
finset.prod_attach_univ
{α : Type u_1}
{β : Type u_2}
[fintype α]
[comm_monoid β]
(f : {a // a ∈ finset.univ} → β) :
∏ (x : {x // x ∈ finset.univ}) in finset.univ.attach, f x = ∏ (x : α), f ⟨x, _⟩
@[simp]
theorem
finset.sum_attach_univ
{α : Type u_1}
{β : Type u_2}
[fintype α]
[add_comm_monoid β]
(f : {a // a ∈ finset.univ} → β) :
∑ (x : {x // x ∈ finset.univ}) in finset.univ.attach, f x = ∑ (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) → β) :
∏ (x : Π (a : α), a ∈ finset.univ → δ a) in finset.univ.pi t, f x = ∏ (x : Π (a : α), δ a) in fintype.pi_finset t, 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) → β) :
∑ (x : Π (a : α), a ∈ finset.univ → δ a) in finset.univ.pi t, f x = ∑ (x : Π (a : α), δ a) in fintype.pi_finset t, 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 → β} :
∏ (a : α), ∑ (b : δ a) in t a, f a b = ∑ (p : Π (a : α), δ a) in fintype.pi_finset t, ∏ (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) :
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 : β → γ) :
∑ (i : α), g (f i) = ∑ (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 : β → γ) :
∏ (i : α), g (f i) = ∏ (i : β), g i
theorem
equiv.sum_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[fintype α]
[fintype β]
[add_comm_monoid γ]
(e : α ≃ β)
(f : β → γ) :
theorem
equiv.prod_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[fintype α]
[fintype β]
[comm_monoid γ]
(e : α ≃ β)
(f : β → γ) :
theorem
fin.sum_univ_eq_sum_range
{α : Type u_1}
[add_comm_monoid α]
(f : ℕ → α)
(n : ℕ) :
∑ (i : fin n), f ↑i = ∑ (i : ℕ) in finset.range n, f i
theorem
fin.prod_univ_eq_prod_range
{α : Type u_1}
[comm_monoid α]
(f : ℕ → α)
(n : ℕ) :
∏ (i : fin n), f ↑i = ∏ (i : ℕ) in finset.range n, f i
It is equivalent to sum a function over fin n or finset.range n.
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) :
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) :
theorem
finset.prod_fiberwise
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[decidable_eq β]
[fintype β]
[comm_monoid γ]
(s : finset α)
(f : α → β)
(g : α → γ) :
∏ (b : β), ∏ (a : α) in finset.filter (λ (a : α), f a = b) s, g a = ∏ (a : α) in s, 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 : α → γ) :
∑ (b : β), ∑ (a : α) in finset.filter (λ (a : α), f a = b) s, g a = ∑ (a : α) in s, g a
theorem
fintype.sum_fiberwise
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[fintype α]
[decidable_eq β]
[fintype β]
[add_comm_monoid γ]
(f : α → β)
(g : α → γ) :
theorem
fintype.prod_fiberwise
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[fintype α]
[decidable_eq β]
[fintype β]
[comm_monoid γ]
(f : α → β)
(g : α → γ) :
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 → β) :
theorem
fintype.prod_sum_elim
{α₁ : Type u_4}
{α₂ : Type u_5}
{M : Type u_6}
[fintype α₁]
[fintype α₂]
[comm_monoid M]
(f : α₁ → M)
(g : α₂ → M) :
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) :