OAI/NumberTheory/CubicMoment/Theta/CubicThetaProjectedContour.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Smooth contour motion for the actual nonzero angular additive series. Both analyticity and polynomial growth are derived from the arithmetic theta transformation. The scale may be any positive real number.

  1. theorem OAI.CubicFirstMoment.cubicThetaSelectedDirichlet_contour line 14