OAI/NumberTheory/Ostmann/ZeroDensity/ComplexCharacterHadamard.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual real-part Hadamard identity for complex characters

  1. def OAI.Ostmann.characterRealZeroSum line 14
  2. theorem OAI.Ostmann.character_real_zero_summable line 17
  3. theorem OAI.Ostmann.character_completed_partial_real_limit line 36
  4. theorem OAI.Ostmann.character_real_zero_self_reflection line 50
  5. theorem OAI.Ostmann.complex_character_hadamard_identity line 73

    Source documentation

    The conjugate functional equation cancels the constant term, yielding the actual zero sum used in the full-height zero-free argument.

    theorem complex_character_hadamard_identity (χ : PrimitiveComplexCharacter) (s : ℂ)
    (hs : 1 < s.re) (hs2 : s.re ≤ 2) :
    characterRealZeroSum χ s = (logDeriv χ.completed s).re +
      (1 / 2) * Real.log χ.modulus := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.characterRealZeroSum