Finite covers from uniform local density

If a uniformly chosen test misses each obligation with probability at most p / q, then t tests suffice whenever card W * p ^ t < q ^ t. The argument counts finite function spaces and uses a union bound; no measure-theoretic or independence assumptions are left to the caller.

theorem Algebraic.Combinatorics.FiniteCover.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

A finite probabilistic cover bound, stated with integer cardinalities.