OAI/NumberTheory/CubicMoment/Estimates/SemiprimeGaussTailPartition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact smooth coordinate partition of each literal semiprime Gauss window. The finite prime cutoff and the original product envelope are retained.

  1. def OAI.CubicFirstMoment.semiprimeGaussTailPiece line 14
  2. theorem OAI.CubicFirstMoment.scaleFirstTailSemiprimeWindow_partition line 19
  3. lemma OAI.CubicFirstMoment.scaleFirstTailKernel_large_factor line 43
  4. theorem OAI.CubicFirstMoment.semiprimeGaussTailPiece_full_support line 57
  5. lemma OAI.CubicFirstMoment.semiprimeGaussTailPiece_window line 95