OAI/NumberTheory/CubicMoment/Estimates/CenteredProductHeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The low-height integral of a literal centered product polynomial. The product envelope is separated at its actual Mellin frequency.

  1. theorem OAI.CubicFirstMoment.centered_product_low_integral line 13
  2. theorem OAI.CubicFirstMoment.centered_product_low_mellin line 46