eulerPrimeLogDerivTermComplex_summable

formal source

 532/-- The complex Euler log-derivative terms are summable on `Re(s) > 1/2`.
 533Lifts `carrierDerivBound_summable` to the complex setting via the
 534per-prime domination bound. -/
 535theorem eulerPrimeLogDerivTermComplex_summable {s : ℂ} (hs : 1/2 < s.re) :
 536    Summable (fun p : Nat.Primes => eulerPrimeLogDerivTermComplex p s) := by
 537  refine Summable.of_norm ?_
 538  exact (carrierDerivBound_summable hs).of_nonneg_of_le
 539    (fun _ => norm_nonneg _)
 540    (fun p => norm_eulerPrimeLogDerivTermComplex_le_carrierDerivTerm (by linarith) p)
 541
 542/-! ### §5d. Meromorphic order of ζ⁻¹ and quantitative factorization -/
 543
 544/-- `riemannZeta` is analytic at every `s ≠ 1`. Uses `DifferentiableOn.analyticAt`
 545from Mathlib's complex Cauchy integral theory. -/
 546theorem analyticAt_riemannZeta {s : ℂ} (hs : s ≠ 1) :
 547    AnalyticAt ℂ riemannZeta s := by
 548  have hdiff : DifferentiableOn ℂ riemannZeta {(1 : ℂ)}ᶜ :=
 549    fun z hz => (differentiableAt_riemannZeta hz).differentiableWithinAt
 550  exact hdiff.analyticAt (isOpen_compl_singleton.mem_nhds hs)
 551
 552/-- `zetaReciprocal` is meromorphic at every point of the strip (away from `s=1`).
 553This follows from `riemannZeta` being analytic at `s ≠ 1` and the inverse
 554of a meromorphic function being meromorphic. -/
 555theorem zetaReciprocal_meromorphicAt (s : ℂ) (hs : s ≠ 1) :
 556    MeromorphicAt zetaReciprocal s := by
 557  show MeromorphicAt (fun z => (riemannZeta z)⁻¹) s
 558  exact (analyticAt_riemannZeta hs).meromorphicAt.inv
 559
 560/-- The meromorphic order of `ζ⁻¹` is the negative of the order of `ζ`.
 561This is a direct consequence of Mathlib's `meromorphicOrderAt_inv`. -/
 562theorem meromorphicOrderAt_zetaReciprocal (s : ℂ) :
 563    meromorphicOrderAt zetaReciprocal s = -meromorphicOrderAt riemannZeta s := by
 564  show meromorphicOrderAt (fun z => (riemannZeta z)⁻¹) s = _
 565  exact meromorphicOrderAt_inv