Proof of `Small-union weighted double-cover estimate`
groundedproofs/Lax253009Proofs/SmallUnionDoubleCovers.lean · lax-253009
What this proof establishes
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
Extract a double subcover of size 2t, sum over the choices of its positions, and bound each remaining support by the total coefficient mass on subsets of its union. The extracted tuples are controlled by the double-cover bound.