OAI/NumberTheory/Ostmann/ZeroDensity/CharacterZerosInfinite.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Infinitely many actual nontrivial zeros for every primitive character

  1. theorem OAI.Ostmann.PrimitiveComplexCharacter.zeros_infinite line 15

    Source documentation

    A finite zero set would force bounded logarithmic derivative, contradicting its Gamma-factor growth along the positive real axis.

    theorem PrimitiveComplexCharacter.zeros_infinite (χ : PrimitiveComplexCharacter) :
    (complexCharacterZeros χ).Infinite := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.complexCharacterZeros