OAI/NumberTheory/CubicMoment/Estimates/GramMellinTwist.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact conversion of the existing Poisson/Mellin kernel's Fourier frequency to the norm heights used by the proved structured moments.

  1. lemma OAI.CubicFirstMoment.gramMellinPhase_eq_mellinPhase line 13
  2. lemma OAI.CubicFirstMoment.mellinPhase_add_height line 21
  3. lemma OAI.CubicFirstMoment.gramMellinPhase_ratio line 28
  4. lemma OAI.CubicFirstMoment.fullStructuredPrimeSum_gram_twist line 39