OAI/NumberTheory/Ostmann/Characters/CharacterMellinIntegral.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The bounded-prefix Mellin representation on Re(s)>0

  1. def OAI.Ostmann.characterSummatory line 16
  2. theorem OAI.Ostmann.characterSummatory_zero line 20
  3. theorem OAI.Ostmann.characterSummatory_bound line 23
  4. theorem OAI.Ostmann.characterSummatory_locallyIntegrable line 30
  5. theorem OAI.Ostmann.characterSummatory_bigO line 44
  6. theorem OAI.Ostmann.characterSummatory_zero_bigO line 50
  7. theorem OAI.Ostmann.characterSummatory_mellin line 57
  8. def OAI.Ostmann.characterMellinL line 75
  9. theorem OAI.Ostmann.characterMellinL_differentiableAt line 78
  10. theorem OAI.Ostmann.characterMellinL_eq_L line 86