Proof of `The size of the decoding set from large coefficients`
groundedproofs/Lax253009Proofs/SmallSupport.lean · lax-253009
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
Bound the union by the sum of support sizes, charge each support at least ℓδ squared mass, and use the total squared-mass bound.