OAI/NumberTheory/CubicMoment/Decomposition/StoppedProductModelTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete complementary Mellin integral of the literal squarefree product model. The actual inverse-sixth norm weight gives the correct length power before rapid decay is applied.

  1. theorem OAI.CubicFirstMoment.stopped_product_model_mellin_tail line 14