OAI/NumberTheory/CubicMoment/Angular/AngularGaussTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal fixed-angular Gauss height tail is negligible. One stopping exponent and one height cap serve all four branches and the semiprime term.

  1. theorem OAI.CubicFirstMoment.primeProductGaussTail_angular_isLittleO line 16