Exact Capture Count Distribution

Abstract

Every finite capture-count value has an exact alternating-sum product mass.

Theorem 1.1 (Exact mass of j captured addresses).

$$\forall j\in \mathbb{N},(\forall b,\sum _y{q}_b(y)=1)\Rightarrow \mathrm{eventProbability}\left(q,\{s\mid |\{a\in A\mid \mathrm{Captured}\left(f,s,a\right)\}|=j\}\right)=\sum _{S\subseteq A,|S|=j}\sum _{U\subseteq A\setminus S}(-1{)}^{|U|}\prod _{b\in A}\mathrm{if}\left(b\in \mathrm{union}\left(S,U\right),\mathrm{fixedPowerMass}\left(q,f,b,|\mathrm{union}\left(S,U\right)|\right),\mathrm{collisionPowerMass}\left(q,f,b,|\mathrm{union}\left(S,U\right)|\right)\right).$$

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

Citation. Gerald Berman and K. D. Fryer (1972). The Inclusion-Exclusion Principle. DOI: 10.1016/b978-0-12-092750-0.50008-9.

Commentary.

Samples with capture count j are partitioned by their exact set S of addresses satisfying the frozen Captured predicate.

For each S, complement inclusion-exclusion over addresses outside S gives the alternating sum over U. The imported exact prescribed-set law evaluates every S union U intersection as the displayed product.

No nonnegativity premise is needed. Normalization is used only by the existing exact product-mass theorem.

References

• Truth anchor: D5/S0/Asymptotics/WeightedProbability/ExactCaptureCount.exact_capture_count_probability
• Dependency: D5/S0/Asymptotics/WeightedProbability/FiniteInclusionExclusion
• Dependency: D5/S0/Asymptotics/WeightedProbability/FiniteProductSetCapture