Proof of `Sublinear bag bounds survive independent blow-ups` (1st statement)
groundedproofs/Lax263307Proofs/BlowUpBagBounds.lean · lax-263307
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
Raise the real sublinear blow-up bag bound to a fixed positive integer power, absorb its constant into a positive integer, and dominate its exponent by a-1 using a(1-beta)>1.