Arbitrary-Order Bonferroni Truncation

Abstract

Every finite Bonferroni truncation bounds weighted escape in the direction determined by its parity.

Theorem 1.1 (Alternating truncations bracket escape).

$$(\forall b,y,0\le q_b(y))\Rightarrow (\mathrm{Even}\left(m\right)\Rightarrow \mathrm{escapeProbability}\left(q,f\right)\le \sum _{0\le r\le m}(-1{)}^r\sum _{T\subseteq A,|T|=r}\mathrm{setCaptureProbability}\left(q,f,T\right))\wedge (\mathrm{Odd}\left(m\right)\Rightarrow \sum _{0\le r\le m}(-1{)}^r\sum _{T\subseteq A,|T|=r}\mathrm{setCaptureProbability}\left(q,f,T\right)\le \mathrm{escapeProbability}\left(q,f\right)).$$

Proof. Machine-checked in Lean as D5/S0/Asymptotics/Bonferroni/TruncationBounds.escape_bonferroni_truncation (✓ std3). ∎

Citation. Janos Galambos (1977). Bonferroni Inequalities. DOI: 10.1214/aop/1176995765.

Commentary.

For each sample, the capture count converts the cardinality-r intersection sum into a binomial coefficient. Mathlib’s exact partial alternating-binomial identity leaves a nonnegative binomial coefficient with sign determined by m.

Nonnegative sample weights preserve the pointwise inequality. No marginal-normalisation hypothesis is needed, so the theorem also applies to nonnegative finite weights whose total mass is not one.

References

• Truth anchor: D5/S0/Asymptotics/Bonferroni/TruncationBounds.escape_bonferroni_truncation
• Dependency: D5/S0/Asymptotics/WeightedProbability/BinomialMomentIdentity
• Dependency: D5/S0/Asymptotics/WeightedProbability/FiniteBonferroni