OAI/NumberTheory/CubicMoment/Theta/CubicThetaCentralPrimeProductSmoothedBilinear.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full Mellin transfer of the published-input prime-product estimate. Both the finite window and its complete complement are controlled, with constants uniform in the independent weights, scales and envelope length.

  1. theorem OAI.CubicFirstMoment.full_prime_centered_smoothed_bilinear_actual line 18