Binomial Moment Identity

Abstract

Every binomial moment of the finite capture count equals the total probability of all prescribed captured subsets of that size.

Theorem 1.1 (Binomial moments enumerate prescribed captured sets).

$$\sum _{0\le j\le |A|}\mathrm{choose}(j,r)\mathrm{eventProbability}\left(q,|C(f)|=j\right)=\sum _{T\subseteq A,|T|=r}\mathrm{setCaptureProbability}\left(q,f,T\right).$$

Proof. Machine-checked in Lean as D5/S0/Asymptotics/WeightedProbability/BinomialMomentIdentity.exact_capture_count_binomial_moment (✓ std3). ∎

Source. Repository-derived.

Commentary.

The identity needs no normalisation hypothesis: it is pure double counting over the finite sample weight. For each sample, the capture-count sum selects its unique realized cardinality. The resulting binomial coefficient counts the r-element subsets of the captured-address finset by Finset.card_powersetCard.

Exchanging the finite sample and subset sums identifies membership in that powerset with simultaneous capture of every address in the prescribed set, yielding setCaptureProbability term by term.

References

• Truth anchor: D5/S0/Asymptotics/WeightedProbability/BinomialMomentIdentity.exact_capture_count_binomial_moment
• Dependency: D5/S0/Asymptotics/WeightedProbability/ExactCaptureCount
• Dependency: D5/S0/Asymptotics/WeightedProbability/FiniteProductSetCapture