OAI/NumberTheory/CubicMoment/Theta/CubicThetaUpperNoStopRow.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_upperTailNoStopRow_finite_bound_proved line 15