English
A combinatorial identity expressing the sum over the powerset in terms of binomial coefficients and cardinalities.
Русский
Комбинаторная тождество выражает сумму по powerset через биномиальные коэффициенты и кардинальности.
LaTeX
$$$\sum_{m\subseteq x} f\#m = \sum_{m=0}^{|x|} { |x| \choose m } f(m)$$$
Lean4
theorem sum_powerset_apply_card {α β : Type*} [AddCommMonoid α] (f : ℕ → α) {x : Finset β} :
∑ m ∈ x.powerset, f #m = ∑ m ∈ range (#x + 1), (#x).choose m • f m :=
by
trans ∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j
· refine (sum_fiberwise_of_maps_to ?_ _).symm
intro y hy
rw [mem_range, Nat.lt_succ_iff]
rw [mem_powerset] at hy
exact card_le_card hy
· refine sum_congr rfl fun y _ ↦ ?_
rw [← card_powersetCard, ← sum_const]
refine sum_congr powersetCard_eq_filter.symm fun z hz ↦ ?_
rw [(mem_powersetCard.1 hz).2]
