OAI/NumberTheory/CubicMoment/Decomposition/StoppedBoundedMellin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The complete Mellin line for bounded squarefree coefficients. All coprimality rows are retained, and the coefficient bound is uniform in both signs and every translated height.

  1. theorem OAI.CubicFirstMoment.bounded_divisor_character_mass line 15
  2. theorem OAI.CubicFirstMoment.bounded_coprime_mellin_integral line 47