OAI/NumberTheory/CubicMoment/Estimates/IdealLogDerivativeMajorant.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform absolute bound on the right Mellin line. Positivity of the actual von Mangoldt coefficients reduces every twist to the principal pole.

  1. theorem OAI.CubicFirstMoment.idealLogDeriv_norm_le_principal line 12
  2. theorem OAI.CubicFirstMoment.idealLogDeriv_uniform_right_line line 44