Source indexedtheorem · leanprover/lean4:v4.32.0

meromorphicOn_eq12_integrand

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:412 to 421

Source documentation

The eq.(12) integrand f(s) = (-ζ'/ζ)(s)·Φ(-s) is meromorphic on the rectangle [-a,1+a]×[-T,T].

Exact Lean statement

theorem meromorphicOn_eq12_integrand {Φ : ℂ → ℂ} {b : ℝ}
    (hΦ : AnalyticOnNhd ℂ Φ {s : ℂ | -(1 + b) < s.re ∧ s.re < b})
    {a T : ℝ} (ha : 0 < a) (hab : a < b) :
    MeromorphicOn (fun s ↦ (-deriv riemannZeta s / riemannZeta s) * Φ (-s))
      (Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem meromorphicOn_eq12_integrand {Φ : ℂ → ℂ} {b : ℝ}    (hΦ : AnalyticOnNhd ℂ Φ {s : ℂ | -(1 + b) < s.re ∧ s.re < b})    {a T : ℝ} (ha : 0 < a) (hab : a < b) :    MeromorphicOn (fun s ↦ (-deriv riemannZeta s / riemannZeta s) * Φ (-s))      (Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I)) := by  intro s₀ hs₀  have hΦan : AnalyticAt ℂ Φ (-s₀) := hΦ (-s₀) (eq12_neg_mem_strip ha hab hs₀)  have hneg : AnalyticAt ℂ (fun s : ℂ ↦ -s) s₀ := analyticAt_id.neg  have hΦneg : MeromorphicAt (fun s ↦ Φ (-s)) s₀ := (hΦan.comp hneg).meromorphicAt  exact (((meromorphicAt_riemannZeta s₀).deriv.neg).div (meromorphicAt_riemannZeta s₀)).mul hΦneg