OAI/NumberTheory/CubicMoment/Estimates/IdealMangoldtContour.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite contour identity for the actual ideal von Mangoldt Mellin integrand. Nonvanishing on the box is supplied by the proved Hecke zero-free region, before estimating its edges.

  1. def OAI.CubicFirstMoment.idealMangoldtMellinIntegrand line 14
  2. lemma OAI.CubicFirstMoment.idealMangoldtMellinIntegrand_differentiableOn line 17
  3. theorem OAI.CubicFirstMoment.idealMangoldt_finite_contour_bound line 31