Finite covers from an exact union bound

If a uniformly chosen test misses each obligation with probability at most p / q, then t tests hit every obligation as soon as |W| p ^ t < q ^ t. The proof counts bad test sequences and takes their union over the obligations, using only finite cardinalities. Density estimates involving exponentials are in the companion FiniteCover module.

Main results

• Cslib.exists_cover_of_scaled_card_lt: the union bound for covers with integer cardinalities.

theorem Cslib.exists_cover_of_scaled_card_lt {S : Type u_1} {W : Type u_2} [Fintype S] [Nonempty S] [Fintype W] (hit : S → W → Prop) [DecidableRel hit] (p q t : ℕ) (localBound : ∀ (w : W), q * Fintype.card { s : S // ¬hit s w } ≤ p * Fintype.card S) (small : Fintype.card W * p ^ t < q ^ t) : ∃ (tests : Fin t → S), ∀ (w : W), ∃ (i : Fin t), hit (tests i) w

The union bound for covers, with integer cardinalities: if a uniform test misses each obligation with probability at most p / q, and |W| p ^ t < q ^ t, then some t tests hit every obligation.