OAI/NumberTheory/CubicMoment/Estimates/SemiprimeGaussTailAngularHecke.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual fixed-angular semiprime window from the derived angular Hecke height mean, preserving its full product Mellin envelope.

  1. def OAI.CubicFirstMoment.semiprimeGaussAngularUnitWindow line 14
  2. lemma OAI.CubicFirstMoment.semiprimeGaussTailPiece_eq_angularUnitWindow line 22
  3. theorem OAI.CubicFirstMoment.semiprimeGaussTail_angular_hecke_window line 38