OAI/NumberTheory/CubicMoment/Theta/CubicThetaCentralAngularPrimeProductBilinear.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual convolution on the other side of the prime bilinear estimate supplies its own logarithmic energy bound. This is the form needed after regrouping a fixed large-row prime box.

  1. theorem OAI.CubicFirstMoment.angular_full_prime_centered_product_bilinear_actual line 18