Vandermonde Count for Subsets of an Intersection

This is a finite-set identity expressing a Vandermonde convolution for two fixed subsets.

Let $\alpha$ be a type with decidable equality, let $U$ be a finite subset of $\alpha$, let $d$ be a natural number, and let $F,F'$ be $d$-element subsets of $U$. For each natural number $s$ from $0$ through $d$, count the $s$-element subsets $S$ of $U$ satisfying $S \subseteq F \cap F'$. Then

This identity is a reusable combinatorial summation formula, with the summands counting subsets of the intersection and weighting them by binomial coefficients.

Formalization Note The summation is implemented over Finset.range (d + 1), and the counted families use Finset.powersetCard followed by Finset.filter; binomial coefficients are represented by Nat.choose.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.Tensor. Shown in its original module context. Proof omitted.

theorem sum_choose_mul_card_filter_subset (U : Finset α) {d : ℕ} {F F' : Finset α}
    (hF : F ∈ U.powersetCard d) (hF' : F' ∈ U.powersetCard d) :
    ∑ s ∈ range (d + 1), d.choose s * ((U.powersetCard s).filter fun S => S ⊆ F ∩ F').card =
      (d + (F ∩ F').card).choose d

Module navigation

Module: Analysis/Tensor/Symmetrization.

Previous: card_filter_union_subset · Next: sum_norm_sq_sum_filter.

Source excerpt, lines 196–199 · Frozen source 408915f.