Splitting a sum over the subsets of a finite set #
A sum over all subsets of a finite set s with at least two elements splits into four parts:
the empty set, the singletons, the subsets with at least two elements other than s, and s
itself. This is the bookkeeping behind expansions of the form
∏_{i ∈ s} (1 + x_i) = ∑_{S ⊆ s} ∏_{i ∈ S} x_i, where the four parts are the constant term, the
linear terms, the mixed terms, and the top-degree term.
Main results #
TauCeti.sum_powerset_eq_add_sum_singleton_add_sum_filter_add: the four-part splitting.
theorem
TauCeti.sum_powerset_eq_add_sum_singleton_add_sum_filter_add
{α : Type u_1}
{M : Type u_2}
[DecidableEq α]
[AddCommMonoid M]
{s : Finset α}
(hs : 1 < s.card)
(f : Finset α → M)
:
A sum over the subsets of a finite set s with at least two elements splits into four
parts: the empty set, the singletons, the subsets with at least two elements other than s, and
s itself.