OAI/NumberTheory/CubicMoment/Estimates/CentralProductSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The smooth product kernel permits the exact detector support to be replaced by its full squarefree envelope. No nonzero term is removed.

  1. def OAI.CubicFirstMoment.centralProductEnvelope line 13
  2. lemma OAI.CubicFirstMoment.centralProductEnvelope_spec line 16
  3. theorem OAI.CubicFirstMoment.central_product_support_sum line 22
  4. lemma OAI.CubicFirstMoment.centralRoughProduct_full line 45