OAI/NumberTheory/Ostmann/Characters/CharacterRightLogDerivativeBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform logarithmic derivative bound to the right of two

  1. theorem OAI.Ostmann.character_logDeriv_right_uniform_bound line 12

    Source documentation

    Absolute convergence supplies a single bound for every primitive character.

    theorem character_logDeriv_right_uniform_bound : ∃ C : ℝ, 0 < C ∧
    ∀ (χ : PrimitiveComplexCharacter) (s : ℂ), 2 ≤ s.re → ‖logDeriv χ.L s‖ ≤ C := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter