HalaszGroupedException.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Apply the full triple-convolution estimate to one actual logarithmic band, with its adaptive denominator and finite cofactor prime cutoff.