OAI/NumberTheory/Ostmann/ZeroDensity/RealCharacterZeroConvergence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absolute convergence of the real-axis zero kernel

  1. theorem OAI.Ostmann.real_zero_kernel_square_bound line 10
  2. theorem OAI.Ostmann.real_character_zero_kernel_summable line 40

    Source documentation

    The actual faithful zero family supplies the convergence field of the published real-character Hadamard expansion.

    theorem real_character_zero_kernel_summable (χ : PrimitiveRealCharacter) (s : ℝ)
    (hs : 1 < s) (hs2 : s ≤ 2) :
    Summable (fun i => realZeroKernel (s - ((realCharacterActualZeros χ).zeros i).re)
      ((realCharacterActualZeros χ).zeros i).im) := by
…

    Mentions: OAI.Ostmann.PrimitiveRealCharacter, OAI.Ostmann.realZeroKernel, OAI.Ostmann.realCharacterActualZeros