Big operators

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

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.

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.

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.

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.

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 = 1, ..., #s.

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 = 1, ..., #s

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.

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.