OAI/NumberTheory/CubicMoment/Theta/CubicThetaNoStopNegligible.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual theta transform supplies the angular no-stop estimate. No metaplectic Voronoi premise is used.

  1. theorem OAI.CubicFirstMoment.angular_scaleFirstOrdinaryNoStopTail_isLittleO_proved line 15