OAI/NumberTheory/TwoPoint/ShortIntervals/MRTRieszMangoldt.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The positive quadratic Riesz prime majorant is exactly an integral of the logarithmic derivative of zeta. No cutoff is moved or rounded.

  1. def OAI.TwoPointCorrelations.mrtMangoldtTwist line 14
  2. def OAI.TwoPointCorrelations.mrtZetaRieszIntegrand line 17
  3. lemma OAI.TwoPointCorrelations.mrt_mangoldt_twist_term line 21
  4. lemma OAI.TwoPointCorrelations.mrt_mangoldt_twist_summable line 32
  5. lemma OAI.TwoPointCorrelations.mrt_mangoldt_twist_LSeries line 37
  6. lemma OAI.TwoPointCorrelations.mrt_mangoldt_twist_phase line 44
  7. theorem OAI.TwoPointCorrelations.mrt_riesz_mangoldt_finite_sum line 55
  8. theorem OAI.TwoPointCorrelations.mrt_riesz_prime_kernel_integral line 68