OAI/NumberTheory/Ostmann/Characters/CharacterCompletedOrderOne.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The order-one growth hypothesis for completed character L-functions

  1. theorem OAI.Ostmann.character_completed_order_one line 11

    Source documentation

    Concrete growth in the exact epsilon-family form needed for Hadamard factorization. No abstract growth hypothesis on the L-function is used.

    theorem character_completed_order_one (χ : PrimitiveComplexCharacter) :
    ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 < C ∧ ∀ z : ℂ,
      ‖χ.completed z‖ ≤ Real.exp (C * (1 + ‖z‖) ^ (1 + ε)) := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter