Module docstring
{"# Big operators
In this file we prove theorems about products and sums over a Finset.powerset.
"}
Finset.prod_powerset_insert
theorem
[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)
Full source
/-- 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`. -/
@[to_additive "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`."]
lemma prod_powerset_insert [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) := by
rw [powerset_insert, prod_union, prod_image]
· exact insert_erase_invOn.2.injOn.mono fun t ht ↦ not_mem_mono (mem_powerset.1 ht) ha
· aesop (add simp [disjoint_left, insert_subset_iff])Informal description
Let $\alpha$ be a type with decidable equality, $s$ a finite subset of $\alpha$, and $a \in \alpha$ an element not in $s$. For any commutative monoid $\beta$ and function $f : \text{Finset } \alpha \to \beta$, the product of $f$ over all subsets of $s \cup \{a\}$ equals the product of two terms:
1. The product of $f$ over all subsets of $s$
2. The product of $f$ over all subsets of $s$ with $a$ added to each subset
In symbols:
\[ \prod_{t \subseteq s \cup \{a\}} f(t) = \left(\prod_{t \subseteq s} f(t)\right) \cdot \left(\prod_{t \subseteq s} f(t \cup \{a\})\right) \]
Finset.prod_powerset_cons
theorem
(ha : a ∉ s) (f : Finset α → β) :
∏ t ∈ (s.cons a ha).powerset, f t =
(∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (cons a t <| not_mem_mono (mem_powerset.1 t.2) ha)
Full source
/-- 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`. -/
@[to_additive "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`."]
lemma prod_powerset_cons (ha : a ∉ s) (f : Finset α → β) :
∏ t ∈ (s.cons a ha).powerset, f t = (∏ t ∈ s.powerset, f t) *
∏ t ∈ s.powerset.attach, f (cons a t <| not_mem_mono (mem_powerset.1 t.2) ha) := by
classical
simp_rw [cons_eq_insert]
rw [prod_powerset_insert ha, prod_attach _ fun t ↦ f (insert a t)]Informal description
Let $\alpha$ be a type, $s$ a finite subset of $\alpha$, and $a \in \alpha$ an element not in $s$. For any commutative monoid $\beta$ and function $f : \text{Finset } \alpha \to \beta$, the product of $f$ over all subsets of $\{a\} \cup s$ equals the product of two terms:
1. The product of $f$ over all subsets of $s$
2. The product of $f$ over all subsets of $s$ with $a$ added to each subset (where each subset is paired with its membership proof)
In symbols:
\[ \prod_{t \subseteq \{a\} \cup s} f(t) = \left(\prod_{t \subseteq s} f(t)\right) \cdot \left(\prod_{t \in \mathcal{P}(s)} f(\{a\} \cup t)\right) \]
Finset.prod_powerset
theorem
(s : Finset α) (f : Finset α → β) : ∏ t ∈ powerset s, f t = ∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t
Full source
/-- A product over `powerset s` is equal to the double product over sets of subsets of `s` with
`#s = k`, for `k = 1, ..., #s`. -/
@[to_additive "A sum over `powerset s` is equal to the double sum over sets of subsets of `s` with
`#s = k`, for `k = 1, ..., #s`"]
lemma prod_powerset (s : Finset α) (f : Finset α → β) :
∏ t ∈ powerset s, f t = ∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t := by
rw [powerset_card_disjiUnion, prod_disjiUnion]Informal description
Let $s$ be a finite set of type $\alpha$ and let $f$ be a function from finite subsets of $\alpha$ to a commutative monoid $\beta$. The product of $f$ over all subsets of $s$ equals the product over all possible cardinalities $j$ from $0$ to $|s|$ of the product of $f$ over all subsets of $s$ with exactly $j$ elements.
In symbols:
$$
\prod_{t \subseteq s} f(t) = \prod_{j=0}^{|s|} \prod_{\substack{t \subseteq s \\ |t| = j}} f(t).
$$
Finset.prod_powersetCard
theorem
(n : ℕ) (s : Finset α) (f : ℕ → β) : ∏ t ∈ powersetCard n s, f #t = f n ^ (#s).choose n
Full source
/-- A product over `Finset.powersetCard` which only depends on the size of the sets is constant. -/
@[to_additive
"A sum over `Finset.powersetCard` which only depends on the size of the sets is constant."]
lemma prod_powersetCard (n : ℕ) (s : Finset α) (f : ℕ → β) :
∏ t ∈ powersetCard n s, f #t = f n ^ (#s).choose n := by
rw [prod_eq_pow_card, card_powersetCard]; rintro a ha; rw [(mem_powersetCard.1 ha).2]Informal description
Let $M$ be a commutative monoid, $\alpha$ a type, and $s$ a finite subset of $\alpha$. For any natural number $n$ and any function $f \colon \mathbb{N} \to M$, the product of $f(|t|)$ over all subsets $t \subseteq s$ with exactly $n$ elements is equal to $f(n)$ raised to the power of the binomial coefficient $\binom{|s|}{n}$. In symbols:
$$
\prod_{t \in \text{powersetCard}_n(s)} f(|t|) = f(n)^{\binom{|s|}{n}}.
$$