OAI/NumberTheory/CubicMoment/Estimates/PrimeTailMellinMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The full Mellin envelope preserves a translated height mean. Only a bounded shift range is needed; the complement uses an actual moment of the smooth Mellin weight and the coarse polynomial bound.

  1. theorem OAI.CubicFirstMoment.complex_mellin_height_mean line 14
  2. def OAI.CubicFirstMoment.zeroLineMellinMoment line 54
  3. theorem OAI.CubicFirstMoment.zeroLineMellin_height_mean line 57