OAI/NumberTheory/Ostmann/ZeroDensity/RectangleLogIntegrals.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The reciprocal integral around a rectangle

These explicit logarithmic primitives fix the orientation and the factor 2 * pi * I used by the character contour shift.

  1. def OAI.Ostmann.rectangleBoundaryIntegral line 17
  2. theorem OAI.Ostmann.reciprocal_horizontal_integral line 21
  3. theorem OAI.Ostmann.reciprocal_vertical_integral_right line 40
  4. theorem OAI.Ostmann.reciprocal_vertical_integral_left line 60
  5. theorem OAI.Ostmann.log_neg_of_im_pos line 80
  6. theorem OAI.Ostmann.log_neg_of_im_neg line 86
  7. theorem OAI.Ostmann.rectangleBoundaryIntegral_reciprocal line 92