# Big operators #

In this file we prove theorems about products and sums over a `Finset.powerset`.

source
theorem Finset.prod_powerset_insert {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [CommMonoid β] [DecidableEq α] (ha : a ∉ s) (f : Finset α → β) :
∏ t ∈ (insert a s).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)

A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets of `s`, and over all subsets of `s` to which one adds `x`.

source
theorem Finset.sum_powerset_insert {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [AddCommMonoid β] [DecidableEq α] (ha : a ∉ s) (f : Finset α → β) :
∑ t ∈ (insert a s).powerset, f t = ∑ t ∈ s.powerset, f t + ∑ t ∈ s.powerset, f (insert a t)

A sum over all subsets of `s ∪ {x}` is obtained by summing the sum over all subsets of `s`, and over all subsets of `s` to which one adds `x`.

source
theorem Finset.prod_powerset_cons {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [CommMonoid β] (ha : a ∉ s) (f : Finset α → β) :
∏ t ∈ (cons a s ha).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (cons a ↑t ⋯)

A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets of `s`, and over all subsets of `s` to which one adds `x`.

source
theorem Finset.sum_powerset_cons {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [AddCommMonoid β] (ha : a ∉ s) (f : Finset α → β) :
∑ t ∈ (cons a s ha).powerset, f t = ∑ t ∈ s.powerset, f t + ∑ t ∈ s.powerset.attach, f (cons a ↑t ⋯)

A sum over all subsets of `s ∪ {x}` is obtained by summing the sum over all subsets of `s`, and over all subsets of `s` to which one adds `x`.

source
theorem Finset.prod_powerset {α : Type u_1} {β : Type u_2} [CommMonoid β] (s : Finset α) (f : Finset α → β) :
∏ t ∈ s.powerset, f t = ∏ j ∈ range (s.card + 1), ∏ t ∈ powersetCard j s, f t

A product over `powerset s` is equal to the double product over sets of subsets of `s` with `#s = k`, for `k = 0, ..., #s`.

source
theorem Finset.sum_powerset {α : Type u_1} {β : Type u_2} [AddCommMonoid β] (s : Finset α) (f : Finset α → β) :
∑ t ∈ s.powerset, f t = ∑ j ∈ range (s.card + 1), ∑ t ∈ powersetCard j s, f t

A sum over `powerset s` is equal to the double sum over sets of subsets of `s` with `#s = k`, for `k = 0, ..., #s`

source
theorem Finset.prod_powersetCard {α : Type u_1} {β : Type u_2} [CommMonoid β] (n : ℕ) (s : Finset α) (f : ℕ → β) :
∏ t ∈ powersetCard n s, f t.card = f n ^ s.card.choose n

A product over `Finset.powersetCard` which only depends on the size of the sets is constant.

source
theorem Finset.sum_powersetCard {α : Type u_1} {β : Type u_2} [AddCommMonoid β] (n : ℕ) (s : Finset α) (f : ℕ → β) :
∑ t ∈ powersetCard n s, f t.card = s.card.choose n • f n

A sum over `Finset.powersetCard` which only depends on the size of the sets is constant.