OAI/NumberTheory/CubicMoment/Estimates/GramStructuredRows.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The rows in the Poisson kernel are exactly the full structured prime sums, including the squarefree restriction and the reversal of Mellin height.

  1. def OAI.CubicFirstMoment.fullSquarefreePrimeSupport line 14
  2. lemma OAI.CubicFirstMoment.fullSquarefreePrimeSupport_primary line 19
  3. lemma OAI.CubicFirstMoment.fullPrimeCoefficient_sum_squarefree line 25
  4. lemma OAI.CubicFirstMoment.gramMellinPhase_neg line 37
  5. theorem OAI.CubicFirstMoment.fullStructuredPrimeRow_norm line 43
  6. theorem OAI.CubicFirstMoment.fullStructuredPrimeRow_reverse_norm line 76