OAI/NumberTheory/CubicMoment/Estimates/SemiprimeGaussTailAngularSplit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact local-height separation of the angular semiprime tail. The high part is negligible using all-height dispersion; the low part is left as the literal finite sum to which the angular Hecke mean must be applied.

  1. def OAI.CubicFirstMoment.semiprimeGaussTailAngular line 14
  2. def OAI.CubicFirstMoment.semiprimeGaussTailAngularLow line 18
  3. def OAI.CubicFirstMoment.semiprimeGaussTailAngularHigh line 26
  4. lemma OAI.CubicFirstMoment.semiprimeGaussTailAngular_split line 34
  5. theorem OAI.CubicFirstMoment.semiprimeGaussTailAngularHigh_log_saving line 53
  6. theorem OAI.CubicFirstMoment.semiprimeGaussTailAngularHigh_isLittleO line 123