OAI/NumberTheory/Ostmann/ZeroDensity/SmoothContourResidue.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact local zero contributions in the smooth contour integral

  1. def OAI.Ostmann.smoothContourWeight line 13
  2. theorem OAI.Ostmann.smoothContourWeight_differentiable line 16
  3. theorem OAI.Ostmann.smoothContourWeight_vertical line 21
  4. theorem OAI.Ostmann.smoothContour_zero_residue line 26

    Source documentation

    Every zero contributes its negative analytic multiplicity times the literal Mellin weight. No zero is replaced by a formal pole label.

    theorem smoothContour_zero_residue (χ : PrimitiveComplexCharacter)
    (X : ℝ) (hX : 0 < X) (z : ℂ) :
    Tendsto (fun s => (s - z) *
      ((-deriv χ.L s / χ.L s) * smoothContourWeight X s)) (𝓝[≠] z)
      (𝓝 (-(analyticOrderNatAt χ.L z : ℂ) * smoothContourWeight X z)) := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.smoothContourWeight