OAI/NumberTheory/Ostmann/Characters/CharacterRightHalfPlane.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Quantitative initial bounds for the continued character L-function

The elementary coefficient bounds and Möbius inverse give a uniform positive lower bound on Re(s)=2, used as the center value in the zero-count argument.

  1. theorem OAI.Ostmann.lSeries_norm_bound_re_two line 19
  2. theorem OAI.Ostmann.PrimitiveComplexCharacter.L_bound_re_two line 35
  3. theorem OAI.Ostmann.PrimitiveComplexCharacter.L_lower_re_two line 41
  4. theorem OAI.Ostmann.PrimitiveComplexCharacter.partial_sum_bigO line 66
  5. theorem OAI.Ostmann.PrimitiveComplexCharacter.L_integral_right line 73