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 requiringalgebra.big_operators(and hence many other imports) as a dependency offintype.
However many of the results here really belong in algebra.big_operators.basic
and should be moved at some point.
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 : ι → α) :
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) :
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.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
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 β] :
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} → β) :
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.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 : α → γ) :
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₂))