OAI/NumberTheory/CubicMoment/Estimates/ScaleFirstTailDecompositionEnvelope.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The literal squarefree product cutoff can be removed exactly after retaining the original smooth envelope and Gauss coefficient.

  1. lemma OAI.CubicFirstMoment.scaleFirstTailKernel_zero_off_envelope line 14
  2. lemma OAI.CubicFirstMoment.scaleFirstTailKernel_indicator line 25
  3. theorem OAI.CubicFirstMoment.scaleFirstTailStoppedDyads_envelope line 33