OAI/NumberTheory/Ostmann/Characters/CharacterCompletedDivergence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Growth of the completed logarithmic derivative on the positive real axis

  1. theorem OAI.Ostmann.PrimitiveComplexCharacter.gammaFactor_differentiableAt_pos line 13
  2. theorem OAI.Ostmann.PrimitiveComplexCharacter.completed_logDeriv_eq_add line 32
  3. theorem OAI.Ostmann.completed_logDeriv_sample_re_tendsto line 50

    Source documentation

    The Gamma term dominates the uniformly bounded absolutely convergent L-series term.

    theorem completed_logDeriv_sample_re_tendsto (χ : PrimitiveComplexCharacter) :
    Tendsto (fun n => (logDeriv χ.completed (characterGammaSample χ n)).re) atTop atTop := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.characterGammaSample