OAI/NumberTheory/Ostmann/Characters/CharacterRootNumberBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A sufficient elementary bound for the character root number

  1. theorem OAI.Ostmann.PrimitiveComplexCharacter.rootNumber_norm_le line 14

    Source documentation

    The triangle inequality is sufficient for the growth estimate; no sharp Gauss-sum evaluation is required here.

    theorem PrimitiveComplexCharacter.rootNumber_norm_le (χ : PrimitiveComplexCharacter) :
    ‖@DirichletCharacter.rootNumber χ.modulus ⟨χ.positive.ne'⟩ χ.character‖ ≤ χ.modulus := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter