OAI/NumberTheory/CubicMoment/Estimates/ScaleFirstStoppedTailEnvelope.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact full-line Mellin separation of the total-product envelope in a finite height tail. No Mellin frequency is discarded.

  1. def OAI.CubicFirstMoment.envelopeCutoffBilinearTail line 14
  2. theorem OAI.CubicFirstMoment.envelopeCutoffBilinearTail_mellin line 21
  3. theorem OAI.CubicFirstMoment.envelopeCutoffBilinearTail_bound line 76