OAI/NumberTheory/Ostmann/ZeroDensity/CompletedPartialFractionLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The limit of actual completed-L logarithmic-derivative differences

  1. theorem OAI.Ostmann.completed_partial_fraction_difference_tendsto line 16

    Source documentation

    Subtracting at two fixed nonzero points cancels the constant logarithmic part. This is the exact part of Hadamard factorization needed below.

    theorem completed_partial_fraction_difference_tendsto (χ : PrimitiveComplexCharacter)
    (x y : ℂ) (hx : χ.completed x ≠ 0) (hy : χ.completed y ≠ 0) :
    Tendsto (fun n : ℕ => completedZeroPartialFraction χ ((n : ℝ) + 1) y -
      completedZeroPartialFraction χ ((n : ℝ) + 1) x) atTop
      (𝓝 (logDeriv χ.completed y - logDeriv χ.completed x)) := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.completedZeroPartialFraction