OAI/NumberTheory/CubicMoment/Estimates/ArithmeticMellinKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Convert the Fourier-transform frequency to the arithmetic height in N(n)^(it). The fixed factor 2π stays in the actual kernel.

  1. def OAI.CubicFirstMoment.arithmeticMellinCoefficient line 12
  2. lemma OAI.CubicFirstMoment.arithmeticMellinCoefficient_continuous line 16
  3. lemma OAI.CubicFirstMoment.arithmeticMellinCoefficient_integrable line 22
  4. theorem OAI.CubicFirstMoment.arithmeticMellinCoefficient_quadratic_decay line 28