OAI/NumberTheory/Ostmann/ZeroDensity/CharacterGammaContour.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual character Gamma factors on both vertical contour lines

  1. theorem OAI.Ostmann.contourLine_expanded line 13
  2. theorem OAI.Ostmann.contourLine_shift line 19
  3. theorem OAI.Ostmann.PrimitiveComplexCharacter.gammaFactor_differentiableAt line 27
  4. theorem OAI.Ostmann.characterGamma_contour_bound line 40
  5. theorem OAI.Ostmann.characterGammaInverse_contour_bound line 58