OAI/NumberTheory/CubicMoment/Decomposition/StoppedDivisorMellinTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The entire arithmetic Mellin tail of bounded squarefree coefficients. The mean bound is the proved divisor-weighted low-height theorem, uniformly in the height shift. It needs no prime-cancellation hypothesis.

  1. theorem OAI.CubicFirstMoment.bounded_divisor_arithmetic_mellin_tail line 16