OAI/NumberTheory/CubicMoment/Estimates/CenteredProductMellin.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact Mellin separation of the smooth total-product factor in a centered bilinear Gauss sum. The norm height is shifted by the true Mellin frequency, and absolute integrability follows from the smooth weight.

  1. def OAI.CubicFirstMoment.centeredProductPolynomial line 15
  2. def OAI.CubicFirstMoment.centeredProductSmoothed line 19
  3. theorem OAI.CubicFirstMoment.centered_product_mellin line 24
  4. theorem OAI.CubicFirstMoment.centered_product_mellin_integrable line 62