DilatedRoughShifts.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Rough-shift cancellation for the actual factors b(qn), g(qn). The dilation is unrestricted and its sole cost is the averaged Euler factor.