OAI/NumberTheory/CubicMoment/Theta/CubicThetaActualGaussTails.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal Gauss height tail in every fixed angular mode. All inputs in these tail estimates have now been proved, including the radial pole with its actual constant; no normalization of that pole is assumed.

  1. theorem OAI.CubicFirstMoment.cubicTheta_primeProductGaussTail_isLittleO line 14