OAI/NumberTheory/Ostmann/ZeroDensity/SmoothContourRegularPart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing each actual simple logarithmic-derivative pole

After adding back the zero's exact principal part, the smooth contour integrand agrees locally with an analytic function.

  1. theorem OAI.Ostmann.smoothContour_regular_part line 16