Proof of `A uniform sample is unlikely to miss a large set`
groundedproofs/Lax235315Proofs/ComponentProofs.lean · lax-235315
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The fixed-size sample avoidance estimate holds as a finite counting inequality.
Proof strategy
Count avoiding samples by a binomial coefficient, bound its ratio to all samples by an exponential, and use the ceiling sampling rate and N≤2^L.
Attribution
Lemma 3.7 of Dreier–Kuske, arXiv:2602.14625v1, through the component proof ported from the existing local development at commit 44a44623.