OAI/NumberTheory/Ostmann/ZeroDensity/RectangleGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.contourRectangleBoundary line 10
  2. theorem OAI.Ostmann.contourBoundary_bottom line 14
  3. theorem OAI.Ostmann.contourBoundary_top line 18
  4. theorem OAI.Ostmann.contourBoundary_right line 22
  5. theorem OAI.Ostmann.contourBoundary_left line 26
  6. theorem OAI.Ostmann.rectangleIntegrable_of_continuousOn line 30
  7. theorem OAI.Ostmann.rectangleBoundaryIntegral_congr line 43
  8. theorem OAI.Ostmann.contourBoundary_ne_interior line 52
  9. theorem OAI.Ostmann.rectangleIntegrable_sub_inv line 59
  10. theorem OAI.Ostmann.rectangleBoundaryIntegral_eq_zero line 66