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.BigOperators (and hence many other imports) as a
dependency of Fintype.
However many of the results here really belong in Algebra.BigOperators.Basic
and should be moved at some point.
theorem
Fintype.sum_bool
{α : Type u_1}
[AddCommMonoid α]
(f : Bool → α)
:
(Finset.sum Finset.univ fun b => f b) = f true + f false
theorem
Fintype.prod_bool
{α : Type u_1}
[CommMonoid α]
(f : Bool → α)
:
(Finset.prod Finset.univ fun b => f b) = f true * f false
theorem
Fintype.card_eq_sum_ones
{α : Type u_4}
[Fintype α]
:
Fintype.card α = Finset.sum Finset.univ fun _a => 1
theorem
Fintype.sum_extend_by_zero
{α : Type u_1}
{ι : Type u_4}
[DecidableEq ι]
[Fintype ι]
[AddCommMonoid α]
(s : Finset ι)
(f : ι → α)
:
(Finset.sum Finset.univ fun i => if i ∈ s then f i else 0) = Finset.sum s fun i => f i
theorem
Fintype.prod_extend_by_one
{α : Type u_1}
{ι : Type u_4}
[DecidableEq ι]
[Fintype ι]
[CommMonoid α]
(s : Finset ι)
(f : ι → α)
:
(Finset.prod Finset.univ fun i => if i ∈ s then f i else 1) = Finset.prod s fun i => f i
theorem
Fintype.sum_eq_zero
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[AddCommMonoid M]
(f : α → M)
(h : ∀ (a : α), f a = 0)
:
(Finset.sum Finset.univ fun a => f a) = 0
theorem
Fintype.prod_eq_one
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[CommMonoid M]
(f : α → M)
(h : ∀ (a : α), f a = 1)
:
(Finset.prod Finset.univ fun a => f a) = 1
theorem
Fintype.sum_congr
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[AddCommMonoid M]
(f : α → M)
(g : α → M)
(h : ∀ (a : α), f a = g a)
:
(Finset.sum Finset.univ fun a => f a) = Finset.sum Finset.univ fun a => g a
theorem
Fintype.prod_congr
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[CommMonoid M]
(f : α → M)
(g : α → M)
(h : ∀ (a : α), f a = g a)
:
(Finset.prod Finset.univ fun a => f a) = Finset.prod Finset.univ fun a => g a
theorem
Fintype.sum_eq_single
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[AddCommMonoid M]
{f : α → M}
(a : α)
(h : ∀ (x : α), x ≠ a → f x = 0)
:
(Finset.sum Finset.univ fun x => f x) = f a
theorem
Fintype.prod_eq_single
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[CommMonoid M]
{f : α → M}
(a : α)
(h : ∀ (x : α), x ≠ a → f x = 1)
:
(Finset.prod Finset.univ fun x => f x) = f a
theorem
Fintype.sum_eq_add
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[AddCommMonoid M]
{f : α → M}
(a : α)
(b : α)
(h₁ : a ≠ b)
(h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 0)
:
(Finset.sum Finset.univ fun x => f x) = f a + f b
theorem
Fintype.prod_eq_mul
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[CommMonoid M]
{f : α → M}
(a : α)
(b : α)
(h₁ : a ≠ b)
(h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1)
:
(Finset.prod Finset.univ fun x => f x) = f a * f b
theorem
Fintype.eq_of_subsingleton_of_sum_eq
{M : Type u_4}
[AddCommMonoid M]
{ι : Type u_5}
[Subsingleton ι]
{s : Finset ι}
{f : ι → M}
{b : M}
(h : (Finset.sum s fun i => f i) = b)
(i : ι)
:
If a sum of a Finset of a subsingleton type has a given
value, so do the terms in that sum.
theorem
Fintype.eq_of_subsingleton_of_prod_eq
{M : Type u_4}
[CommMonoid M]
{ι : Type u_5}
[Subsingleton ι]
{s : Finset ι}
{f : ι → M}
{b : M}
(h : (Finset.prod s fun i => f i) = b)
(i : ι)
:
If a product of a Finset of a subsingleton type has a given
value, so do the terms in that product.
@[simp]
theorem
Fintype.sum_option
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[AddCommMonoid M]
(f : Option α → M)
:
(Finset.sum Finset.univ fun i => f i) = f none + Finset.sum Finset.univ fun i => f (some i)
@[simp]
theorem
Fintype.prod_option
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[CommMonoid M]
(f : Option α → M)
:
(Finset.prod Finset.univ fun i => f i) = f none * Finset.prod Finset.univ fun i => f (some i)
@[simp]
theorem
Fintype.card_sigma
{α : Type u_4}
(β : α → Type u_5)
[Fintype α]
[(a : α) → Fintype (β a)]
:
Fintype.card (Sigma β) = Finset.sum Finset.univ fun a => Fintype.card (β a)
@[simp]
theorem
Finset.card_pi
{α : Type u_1}
[DecidableEq α]
{δ : α → Type u_4}
(s : Finset α)
(t : (a : α) → Finset (δ a))
:
Finset.card (Finset.pi s t) = Finset.prod s fun a => Finset.card (t a)
@[simp]
theorem
Fintype.card_piFinset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_4}
(t : (a : α) → Finset (δ a))
:
Finset.card (Fintype.piFinset t) = Finset.prod Finset.univ fun a => Finset.card (t a)
@[simp]
theorem
Fintype.card_pi
{α : Type u_1}
{β : α → Type u_4}
[DecidableEq α]
[Fintype α]
[(a : α) → Fintype (β a)]
:
Fintype.card ((a : α) → β a) = Finset.prod Finset.univ fun a => Fintype.card (β a)
@[simp]
theorem
Fintype.card_fun
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[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.sum_attach_univ
{α : Type u_1}
{β : Type u_2}
[Fintype α]
[AddCommMonoid β]
(f : { a // a ∈ Finset.univ } → β)
:
(Finset.sum (Finset.attach Finset.univ) fun x => f x) = Finset.sum Finset.univ fun x => f { val := x, property := (_ : x ∈ Finset.univ) }
@[simp]
theorem
Finset.prod_attach_univ
{α : Type u_1}
{β : Type u_2}
[Fintype α]
[CommMonoid β]
(f : { a // a ∈ Finset.univ } → β)
:
(Finset.prod (Finset.attach Finset.univ) fun x => f x) = Finset.prod Finset.univ fun x => f { val := x, property := (_ : x ∈ Finset.univ) }
theorem
Finset.sum_univ_pi
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[Fintype α]
[AddCommMonoid β]
{δ : α → Type u_4}
{t : (a : α) → Finset (δ a)}
(f : ((a : α) → a ∈ Finset.univ → δ a) → β)
:
(Finset.sum (Finset.pi Finset.univ t) fun x => f x) = Finset.sum (Fintype.piFinset t) fun x => f fun a x_1 => x a
Taking a sum over univ.pi t is the same as taking the sum over
Fintype.piFinset t. univ.pi t and Fintype.piFinset 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.piFinset t is a Finset (Π a, t a).
theorem
Finset.prod_univ_pi
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[Fintype α]
[CommMonoid β]
{δ : α → Type u_4}
{t : (a : α) → Finset (δ a)}
(f : ((a : α) → a ∈ Finset.univ → δ a) → β)
:
(Finset.prod (Finset.pi Finset.univ t) fun x => f x) = Finset.prod (Fintype.piFinset t) fun x => f fun a x_1 => x a
Taking a product over univ.pi t is the same as taking the product over Fintype.piFinset t.
univ.pi t and Fintype.piFinset 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.piFinset t is a Finset (Π a, t a).
theorem
Finset.prod_univ_sum
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[Fintype α]
[CommSemiring β]
{δ : α → Type u_1}
[(a : α) → DecidableEq (δ a)]
{t : (a : α) → Finset (δ a)}
{f : (a : α) → δ a → β}
:
(Finset.prod Finset.univ fun a => Finset.sum (t a) fun b => f a b) = Finset.sum (Fintype.piFinset t) fun p => Finset.prod Finset.univ fun x => f x (p x)
The product over univ of a sum can be written as a sum over the product of sets,
Fintype.piFinset. Finset.prod_sum is an alternative statement when the product is not
over univ
theorem
Fintype.sum_pow_mul_eq_add_pow
(α : Type u_4)
[Fintype α]
{R : Type u_5}
[CommSemiring R]
(a : R)
(b : R)
:
(Finset.sum Finset.univ fun s => a ^ Finset.card s * b ^ (Fintype.card α - Finset.card s)) = (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 β]
[AddCommMonoid γ]
{f : α → β}
(hf : Function.Bijective f)
(g : β → γ)
:
(Finset.sum Finset.univ fun i => g (f i)) = Finset.sum Finset.univ fun i => g i
theorem
Function.Bijective.prod_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[Fintype β]
[CommMonoid γ]
{f : α → β}
(hf : Function.Bijective f)
(g : β → γ)
:
(Finset.prod Finset.univ fun i => g (f i)) = Finset.prod Finset.univ fun i => g i
theorem
Equiv.sum_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[Fintype β]
[AddCommMonoid γ]
(e : α ≃ β)
(f : β → γ)
:
(Finset.sum Finset.univ fun i => f (↑e i)) = Finset.sum Finset.univ fun i => f i
theorem
Equiv.prod_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[Fintype β]
[CommMonoid γ]
(e : α ≃ β)
(f : β → γ)
:
(Finset.prod Finset.univ fun i => f (↑e i)) = Finset.prod Finset.univ fun i => f i
theorem
Equiv.sum_comp'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[Fintype β]
[AddCommMonoid γ]
(e : α ≃ β)
(f : α → γ)
(g : β → γ)
(h : ∀ (i : α), f i = g (↑e i))
:
(Finset.sum Finset.univ fun i => f i) = Finset.sum Finset.univ fun i => g i
theorem
Equiv.prod_comp'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[Fintype β]
[CommMonoid γ]
(e : α ≃ β)
(f : α → γ)
(g : β → γ)
(h : ∀ (i : α), f i = g (↑e i))
:
(Finset.prod Finset.univ fun i => f i) = Finset.prod Finset.univ fun i => g i
theorem
Fin.sum_univ_eq_sum_range
{α : Type u_1}
[AddCommMonoid α]
(f : ℕ → α)
(n : ℕ)
:
(Finset.sum Finset.univ fun i => f ↑i) = Finset.sum (Finset.range n) fun 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}
[CommMonoid α]
(f : ℕ → α)
(n : ℕ)
:
(Finset.prod Finset.univ fun i => f ↑i) = Finset.prod (Finset.range n) fun i => f i
It is equivalent to compute the product of a function over Fin n or Finset.range n.
theorem
Finset.sum_fin_eq_sum_range
{β : Type u_2}
[AddCommMonoid β]
{n : ℕ}
(c : Fin n → β)
:
(Finset.sum Finset.univ fun i => c i) = Finset.sum (Finset.range n) fun i => if h : i < n then c { val := i, isLt := h } else 0
theorem
Finset.prod_fin_eq_prod_range
{β : Type u_2}
[CommMonoid β]
{n : ℕ}
(c : Fin n → β)
:
(Finset.prod Finset.univ fun i => c i) = Finset.prod (Finset.range n) fun i => if h : i < n then c { val := i, isLt := h } else 1
theorem
Finset.sum_toFinset_eq_subtype
{α : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
[Fintype α]
(p : α → Prop)
[DecidablePred p]
(f : α → M)
:
(Finset.sum (Set.toFinset {x | p x}) fun a => f a) = Finset.sum Finset.univ fun a => f ↑a
theorem
Finset.prod_toFinset_eq_subtype
{α : Type u_1}
{M : Type u_4}
[CommMonoid M]
[Fintype α]
(p : α → Prop)
[DecidablePred p]
(f : α → M)
:
(Finset.prod (Set.toFinset {x | p x}) fun a => f a) = Finset.prod Finset.univ fun a => f ↑a
theorem
Finset.sum_fiberwise
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[DecidableEq β]
[Fintype β]
[AddCommMonoid γ]
(s : Finset α)
(f : α → β)
(g : α → γ)
:
(Finset.sum Finset.univ fun b => Finset.sum (Finset.filter (fun a => f a = b) s) fun a => g a) = Finset.sum s fun a => g a
theorem
Finset.prod_fiberwise
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[DecidableEq β]
[Fintype β]
[CommMonoid γ]
(s : Finset α)
(f : α → β)
(g : α → γ)
:
(Finset.prod Finset.univ fun b => Finset.prod (Finset.filter (fun a => f a = b) s) fun a => g a) = Finset.prod s fun a => g a
theorem
Fintype.sum_fiberwise
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[DecidableEq β]
[Fintype β]
[AddCommMonoid γ]
(f : α → β)
(g : α → γ)
:
(Finset.sum Finset.univ fun b => Finset.sum Finset.univ fun a => g ↑a) = Finset.sum Finset.univ fun a => g a
theorem
Fintype.prod_fiberwise
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[DecidableEq β]
[Fintype β]
[CommMonoid γ]
(f : α → β)
(g : α → γ)
:
(Finset.prod Finset.univ fun b => Finset.prod Finset.univ fun a => g ↑a) = Finset.prod Finset.univ fun a => g a
theorem
Fintype.prod_dite
{α : Type u_1}
{β : Type u_2}
[Fintype α]
{p : α → Prop}
[DecidablePred p]
[CommMonoid β]
(f : (a : α) → p a → β)
(g : (a : α) → ¬p a → β)
:
(Finset.prod Finset.univ fun a => dite (p a) (f a) (g a)) = (Finset.prod Finset.univ fun a => f ↑a (_ : p ↑a)) * Finset.prod Finset.univ fun a => g ↑a (_ : ¬p ↑a)
theorem
Fintype.sum_sum_elim
{α₁ : Type u_4}
{α₂ : Type u_5}
{M : Type u_6}
[Fintype α₁]
[Fintype α₂]
[AddCommMonoid M]
(f : α₁ → M)
(g : α₂ → M)
:
(Finset.sum Finset.univ fun x => Sum.elim f g x) = (Finset.sum Finset.univ fun a₁ => f a₁) + Finset.sum Finset.univ fun a₂ => g a₂
theorem
Fintype.prod_sum_elim
{α₁ : Type u_4}
{α₂ : Type u_5}
{M : Type u_6}
[Fintype α₁]
[Fintype α₂]
[CommMonoid M]
(f : α₁ → M)
(g : α₂ → M)
:
(Finset.prod Finset.univ fun x => Sum.elim f g x) = (Finset.prod Finset.univ fun a₁ => f a₁) * Finset.prod Finset.univ fun a₂ => g a₂
@[simp]
theorem
Fintype.sum_sum_type
{α₁ : Type u_4}
{α₂ : Type u_5}
{M : Type u_6}
[Fintype α₁]
[Fintype α₂]
[AddCommMonoid M]
(f : α₁ ⊕ α₂ → M)
:
(Finset.sum Finset.univ fun x => f x) = (Finset.sum Finset.univ fun a₁ => f (Sum.inl a₁)) + Finset.sum Finset.univ fun a₂ => f (Sum.inr a₂)
@[simp]
theorem
Fintype.prod_sum_type
{α₁ : Type u_4}
{α₂ : Type u_5}
{M : Type u_6}
[Fintype α₁]
[Fintype α₂]
[CommMonoid M]
(f : α₁ ⊕ α₂ → M)
:
(Finset.prod Finset.univ fun x => f x) = (Finset.prod Finset.univ fun a₁ => f (Sum.inl a₁)) * Finset.prod Finset.univ fun a₂ => f (Sum.inr a₂)