OAI/NumberTheory/CubicMoment/Estimates/PrimeTailProductMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A bounded-shift mean for the unsmoothed Gauss polynomial suffices for its actual product envelope. All complementary Mellin frequencies are paid for by an integrable moment, with no frequency discarded.

  1. lemma OAI.CubicFirstMoment.zeroLineMellinMoment_nonneg line 14
  2. theorem OAI.CubicFirstMoment.productGaussSmoothed_height_mean line 19
  3. theorem OAI.CubicFirstMoment.fullPrimeProductSmoothed_height_mean line 38