OAI/NumberTheory/CubicMoment/Theta/CubicThetaCentralPrimeProductBilinear.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.full_prime_centered_product_bilinear_actual line 17