OAI/NumberTheory/CubicMoment/Estimates/PrimeTailMellinScale.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Eight Mellin moments at B^(1/4) absorb the coarse product mass throughout A <= B². The remaining factor B^(-1) pays for any fixed log.

  1. lemma OAI.CubicFirstMoment.primeTail_mellin_error_scale line 11