Finite covers from uniform local density #
If a uniformly chosen test misses each of the obligations w : W with probability at most p / q,
then t tests hit every obligation as soon as |W| p ^ t < q ^ t
(exists_cover_of_scaled_card_lt): the bad sequences of tests are counted, with a union bound
over the obligations. In particular, if every obligation is hit by at least a 1 / q fraction of
the tests, then q (n + 1) tests hit 2 ^ n obligations (exists_cover_of_density).
The exact bound is reexported from FiniteCover.Basic, so finite-only clients need not import
the exponential estimates used for the density corollary.
Main results #
Cslib.exists_cover_of_scaled_card_lt: the union bound for covers.Cslib.exists_cover_of_density: covers from density.
theorem Cslib.exists_cover_of_density {S : Type u_1} {W : Type u_2} [Fintype S] [Nonempty S] [Fintype W] (hit : S → W → Prop) [DecidableRel hit] (q n : ℕ) (hq : 0 < q) (hw : Fintype.card W ≤ 2 ^ n) (density : ∀ (w : W), Fintype.card S ≤ q * Fintype.card { s : S // hit s w }) :
Covers from density: if every obligation w is hit by at least a 1 / q fraction of the
tests, then q (n + 1) tests, with repetitions, hit all of at most 2 ^ n obligations.