OAI/NumberTheory/Ostmann/ZeroDensity/RieszLeftEstimate.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The bounded left vertical segment of the Riesz contour

  1. def OAI.Ostmann.rieszLineMajorant line 11
  2. theorem OAI.Ostmann.rieszLineMajorant_nonneg line 13
  3. theorem OAI.Ostmann.rieszLineMajorant_integrable line 17
  4. theorem OAI.Ostmann.rieszMellinKernel_half_strip line 24
  5. theorem OAI.Ostmann.leftRieszIntegrand_segment_bound line 45