OAI/NumberTheory/Ostmann/Characters/CharacterLogDerivativeLeft.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic derivative on the left side of the explicit-formula contour

  1. theorem OAI.Ostmann.character_logDeriv_left_bound line 13

    Source documentation

    A uniform polynomial bound, derived from the functional equation and the absolutely convergent right-hand line.

    theorem character_logDeriv_left_bound : ∃ C : ℝ, 0 < C ∧
    ∀ (χ : PrimitiveComplexCharacter) (s : ℂ), s.re = -(1 / 2 : ℝ) →
      ‖logDeriv χ.L s‖ ≤ C * (1 + Real.log (χ.modulus : ℝ) + |s.im|) := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter