HalaszDoubleException.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Sum the actual geometric prime bands. The central terms retain the Halász saving, and both kinds of error have summable band weights.

theorem OAI.TwoPointCorrelations.halasz_double_convolution_exception line 14