OAI/NumberTheory/CubicMoment/Estimates/ScaleFirstHighSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The complete manuscript high-scale branch is negligible. The new middle interval is treated by its distinguished group; the higher interval is exactly the already proved large-row high sum.

  1. lemma OAI.CubicFirstMoment.scaleFirstPrimeTuplePiece_eq_high line 15
  2. def OAI.CubicFirstMoment.scaleFirstHighSum line 26
  3. lemma OAI.CubicFirstMoment.scaleFirstHighSum_split line 31
  4. theorem OAI.CubicFirstMoment.scaleFirstHighSum_isLittleO line 48