Skewed Capture and Escape Bounds

Abstract

Independent finite listings with column marginals q_b obey the exact skewed capture formulas, two-sided Bonferroni escape bounds, the uniform kernel, and the one-address edge.

Theorem 1.1 (Skewed exact capture laws and escape bounds).

$$(\forall b,y,0\le q_b(y)\wedge \forall b,\sum _y{q}_b(y)=1)\Rightarrow (\forall a,P\left(E_a\right)={\phi }_a\prod _{b\ne a}{c}_b\wedge \forall a,a^{\prime },a\ne a^{\prime }\Rightarrow \mathrm{Ppair}\left(a,a^{\prime }\right)=\mathrm{fixedSquareMass}\left(q,f,a\right)\mathrm{fixedSquareMass}\left(q,f,a^{\prime }\right)\prod _{b\ne a,b\ne a^{\prime }}\mathrm{collisionSquareMass}\left(q,f,b\right)\wedge 1-\sum _{a}P\left(E_a\right)\le \mathrm{Pescape}\left(q,f\right)\le 1-\sum _{a}P\left(E_a\right)+\sum _{a<a^{\prime }}\mathrm{Ppair}\left(a,a^{\prime }\right)\wedge (\forall a,P\left(q^{\mathrm{unif}},E_a\right)=k{n}^{-A}\wedge \forall a,a^{\prime },a\ne a^{\prime }\Rightarrow \mathrm{Ppair}\left(q^{\mathrm{unif}},a,a^{\prime }\right)=P\left(q^{\mathrm{unif}},E_a\right)P\left(q^{\mathrm{unif}},E_{a^{\prime }}\right))\wedge \forall q^1:\mathrm{Fin}(1)\to Y\to \mathbb{R},(\forall b,y,0\le q_b^1(y)\wedge \forall b,\sum _y{q}_b^1(y)=1)\Rightarrow \mathrm{Pescape}\left(q^1,f\right)=1-\mathrm{fixedMass}\left(q^1,f,0\right).$$

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

Source. Repository-derived.

Commentary.

The address type is finite and linearly ordered only to write each unordered pair once as a<a’. Every matrix cell in column b is an independent draw with nonnegative normalized mass q_b.

Here phi_a is fixedMass q f a, c_b is collisionMass q f b, and their superscript-two forms are fixedSquareMass and collisionSquareMass. The finite-product dependency proves the two exact event formulas.

Pointwise first- and second-order Bonferroni inequalities are multiplied by the nonnegative listing weights and summed. For uniform marginals, q^unif is the constant marginal (b,y) |-> 1/n, k is card(Fix f), n is card(Y), and A is card(Address). The final clause quantifies separately over every nonnegative normalized Fin(1) marginal q^1; its fixedMass at address zero is the source’s phi_0.

Thus the effective equivalent-mutant quantity is the weighted fixed-point mass q(Fix f), not the alphabet cardinality. No bijectivity assumption is placed on f.

References

• Truth anchor: D5/S0/Asymptotics/WeightedProbability/SkewedCaptureBounds.skewed_capture_bounds
• Dependency: D5/S0/Asymptotics/WeightedProbability/FiniteBonferroni