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, but was moved here to avoid
requiring algebra.big_operators (and hence many other imports) as a
dependency of fintype.
theorem
fintype.card_eq_sum_ones
{α : Type u_1}
[fintype α] :
fintype.card α = finset.univ.sum (λ (a : α), 1)
theorem
fintype.sum_extend_by_zero
{α : Type u_1}
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
[add_comm_monoid α]
(s : finset ι)
(f : ι → α) :
theorem
fintype.prod_extend_by_one
{α : Type u_1}
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
[comm_monoid α]
(s : finset ι)
(f : ι → α) :
theorem
fintype.sum_eq_zero
{α : Type u_1}
{M : Type u_4}
[fintype α]
[add_comm_monoid M]
(f : α → M) :
(∀ (a : α), f a = 0) → finset.univ.sum (λ (a : α), f a) = 0
theorem
fintype.prod_eq_one
{α : Type u_1}
{M : Type u_4}
[fintype α]
[comm_monoid M]
(f : α → M) :
(∀ (a : α), f a = 1) → finset.univ.prod (λ (a : α), f a) = 1
theorem
fintype.prod_congr
{α : Type u_1}
{M : Type u_4}
[fintype α]
[comm_monoid M]
(f g : α → M) :
(∀ (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) :
(∀ (a : α), f a = g a) → finset.univ.sum (λ (a : α), f a) = finset.univ.sum (λ (a : α), g a)
theorem
fintype.sum_unique
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
[unique β]
(f : β → M) :
finset.univ.sum (λ (x : β), f x) = f (inhabited.default β)
theorem
fintype.prod_unique
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
[unique β]
(f : β → M) :
finset.univ.prod (λ (x : β), f x) = f (inhabited.default β)
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 : ι) :
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 : ι) :
If a sum of a finset of a subsingleton type has a given
value, so do the terms in that sum.
theorem
fin.prod_univ_succ
{β : Type u_2}
[comm_monoid β]
{n : ℕ}
(f : fin n.succ → β) :
finset.univ.prod (λ (i : fin n.succ), f i) = f 0 * finset.univ.prod (λ (i : fin n), f i.succ)
@[simp]
theorem
fin.prod_univ_zero
{β : Type u_2}
[comm_monoid β]
(f : fin 0 → β) :
finset.univ.prod (λ (i : fin 0), f i) = 1
@[simp]
theorem
fin.sum_univ_zero
{β : Type u_2}
[add_comm_monoid β]
(f : fin 0 → β) :
finset.univ.sum (λ (i : fin 0), f i) = 0
theorem
fin.sum_univ_succ
{β : Type u_2}
[add_comm_monoid β]
{n : ℕ}
(f : fin n.succ → β) :
finset.univ.sum (λ (i : fin n.succ), f i) = f 0 + finset.univ.sum (λ (i : fin n), f i.succ)
@[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_sum
(α : Type u_1)
(β : Type u_2)
[fintype α]
[fintype β] :
fintype.card (α ⊕ β) = fintype.card α + fintype.card β
@[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 = 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.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, _⟩)
@[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, _⟩)
theorem
finset.sum_range_eq_sum_fin
{β : Type u_2}
[add_comm_monoid β]
(n : ℕ)
(f : ℕ → β) :
(finset.range n).sum (λ (k : ℕ), f k) = finset.univ.sum (λ (k : fin n), f ↑k)
theorem
finset.prod_range_eq_prod_fin
{β : Type u_2}
[comm_monoid β]
(n : ℕ)
(f : ℕ → β) :
(finset.range n).prod (λ (k : ℕ), f k) = finset.univ.prod (λ (k : fin n), f ↑k)
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
fin.prod_univ_eq_prod_range
{α : Type u_1}
[comm_monoid α]
(f : ℕ → α)
(n : ℕ) :
finset.univ.prod (λ (i : fin n), f i.val) = (finset.range n).prod (λ (i : ℕ), f i)
It is equivalent to sum a function over fin n or finset.range n.
theorem
fin.sum_univ_eq_sum_range
{α : Type u_1}
[add_comm_monoid α]
(f : ℕ → α)
(n : ℕ) :
finset.univ.sum (λ (i : fin n), f i.val) = (finset.range n).sum (λ (i : ℕ), f i)
theorem
finset.sum_equiv
{α : 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
finset.prod_equiv
{α : 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
finset.sum_subtype
{α : Type u_1}
{M : Type u_2}
[add_comm_monoid M]
{p : α → Prop}
{F : fintype (subtype p)}
{s : finset α}
(h : ∀ (x : α), x ∈ s ↔ p x)
(f : α → M) :
theorem
finset.prod_subtype
{α : Type u_1}
{M : Type u_2}
[comm_monoid M]
{p : α → Prop}
{F : fintype (subtype p)}
{s : finset α}
(h : ∀ (x : α), x ∈ s ↔ p x)
(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.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₂))
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₂))
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_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_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.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)