OAI/NumberTheory/Ostmann/ZeroDensity/SmoothLeftContourWeight.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

An integrable majorant for the left vertical contour

  1. def OAI.Ostmann.leftContourLine line 13
  2. theorem OAI.Ostmann.leftContourLine_re line 15
  3. theorem OAI.Ostmann.leftContourLine_im line 18
  4. theorem OAI.Ostmann.leftContourLine_continuous line 21
  5. def OAI.Ostmann.leftContourIntegrand line 25
  6. def OAI.Ostmann.leftContourMajorant line 29
  7. theorem OAI.Ostmann.leftContourMajorant_nonneg line 31
  8. theorem OAI.Ostmann.leftContourMajorant_integrable line 33
  9. theorem OAI.Ostmann.leftContourWeight_norm line 40
  10. theorem OAI.Ostmann.leftContourIntegrand_continuous line 47
  11. theorem OAI.Ostmann.leftContourIntegrand_bound line 59