OAI/NumberTheory/TwoPoint/ShortIntervals/MRTRieszKernel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A positive quadratic Riesz weight and its exact Mellin kernel. The third denominator gives the additional decay needed by sparse prime duality.

  1. def OAI.TwoPointCorrelations.mrtRieszSquare line 13
  2. def OAI.TwoPointCorrelations.mrtRieszKernel line 16
  3. lemma OAI.TwoPointCorrelations.mrt_riesz_square_hasMellin line 19
  4. lemma OAI.TwoPointCorrelations.mrt_riesz_square_continuous line 64
  5. lemma OAI.TwoPointCorrelations.mrt_riesz_kernel_factor line 68
  6. lemma OAI.TwoPointCorrelations.mrt_riesz_kernel_vertical line 74
  7. lemma OAI.TwoPointCorrelations.mrt_riesz_kernel_integrable line 89
  8. lemma OAI.TwoPointCorrelations.mrt_riesz_square_verticalIntegrable line 121
  9. theorem OAI.TwoPointCorrelations.mrt_riesz_inversion line 130