OAI/NumberTheory/CubicMoment/Estimates/MellinPrimeControl.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The two Mellin moments and the edge decay needed for prime contour shifts are controlled by finitely many norms of the logarithmic cutoff.

  1. structure OAI.CubicFirstMoment.PrimeMellinControl line 12
  2. theorem OAI.CubicFirstMoment.primeMellinControl_finite_seminorm line 21