OAI/NumberTheory/CubicMoment/Estimates/SemiprimeGaussTailWeights.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Both analytic height ranges on the original smooth rough-prime weights. The parameter families retain their actual transition ratios.

  1. abbrev OAI.CubicFirstMoment.SemiprimeTailParameters line 14
  2. def OAI.CubicFirstMoment.semiTailLeft line 15
  3. def OAI.CubicFirstMoment.semiTailRight line 16
  4. def OAI.CubicFirstMoment.semiTailLeftWeight line 17
  5. def OAI.CubicFirstMoment.semiTailRightWeight line 19
  6. def OAI.CubicFirstMoment.semiTailLeftFamily line 22
  7. def OAI.CubicFirstMoment.semiTailRightFamily line 29
  8. def OAI.CubicFirstMoment.semiprimeGaussUnitWindow line 36
  9. def OAI.CubicFirstMoment.semiprimeGaussUnitTail line 44
  10. lemma OAI.CubicFirstMoment.semiprimeGaussTailPiece_eq_unitWindow line 52
  11. theorem OAI.CubicFirstMoment.semiprimeGaussTail_hecke_window line 68
  12. theorem OAI.CubicFirstMoment.semiprimeGaussTail_middle_tail line 104
  13. theorem OAI.CubicFirstMoment.semiprimeGaussTail_middle_window line 132