OAI/NumberTheory/Ostmann/Characters/CharacterMellinBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A quantitative bound in the positive half-plane

The bounded periodic prefix sums give the polynomial growth needed for local Jensen estimates, without assuming a convexity estimate for L.

  1. theorem OAI.Ostmann.PrimitiveComplexCharacter.L_integral_positive line 16
  2. theorem OAI.Ostmann.PrimitiveComplexCharacter.L_norm_bound_positive line 23