OAI/NumberTheory/Ostmann/ZeroDensity/RieszMellinKernel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A single integral of the Chebyshev sum

The continuous weight max(1-u,0) has Mellin transform 1/(s(s+1)). This is the one-sided smoothing needed to recover the sharp progression count.

  1. def OAI.Ostmann.rieszPrimeTest line 17
  2. def OAI.Ostmann.rieszMellinKernel line 19
  3. theorem OAI.Ostmann.rieszPrimeTest_continuous line 21
  4. theorem OAI.Ostmann.rieszPrimeTest_hasMellin line 25
  5. theorem OAI.Ostmann.rieszMellinKernel_line_bound line 61