OAI/NumberTheory/CubicMoment/Estimates/ScaleFirstTailDecomposition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact prime detection on each original high-height window. The smooth total-product envelope and the finite squarefree support are retained.

  1. def OAI.CubicFirstMoment.scaleFirstTailKernel line 14
  2. def OAI.CubicFirstMoment.scaleFirstTailRoughWindow line 19
  3. def OAI.CubicFirstMoment.scaleFirstTailSemiprimeWindow line 23
  4. lemma OAI.CubicFirstMoment.scaleFirstTailKernel_envelope_zero line 27
  5. lemma OAI.CubicFirstMoment.scaleFirstTailKernel_norm_range line 31
  6. lemma OAI.CubicFirstMoment.primeProductGaussTail_window_sum line 45
  7. lemma OAI.CubicFirstMoment.scaleFirstTailKernel_prime_support line 57
  8. theorem OAI.CubicFirstMoment.scaleFirstTailWindow_detector line 77
  9. theorem OAI.CubicFirstMoment.primeProductGaussTail_detector line 92
  10. lemma OAI.CubicFirstMoment.scaleFirstTail_envelope_sum line 105
  11. lemma OAI.CubicFirstMoment.scaleFirstTailRoughWindow_full line 128