Source indexedtheorem · leanprover/lean4:v4.32.0

hasSimplePolesOn_eq12_integrand

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:425 to 443

Source documentation

The eq.(12) integrand has at most simple poles on the rectangle: its meromorphic order is ≥ -1 at every point (the -ζ'/ζ factor contributes ≥ -1, the analytic Φ(-·) factor ≥ 0).

Exact Lean statement

theorem hasSimplePolesOn_eq12_integrand {Φ : ℂ → ℂ} {b : ℝ}
    (hΦ : AnalyticOnNhd ℂ Φ {s : ℂ | -(1 + b) < s.re ∧ s.re < b})
    {a T : ℝ} (ha : 0 < a) (hab : a < b) :
    HasSimplePolesOn (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 hasSimplePolesOn_eq12_integrand {Φ : ℂ → ℂ} {b : ℝ}    (hΦ : AnalyticOnNhd ℂ Φ {s : ℂ | -(1 + b) < s.re ∧ s.re < b})    {a T : ℝ} (ha : 0 < a) (hab : a < b) :    HasSimplePolesOn (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_an : AnalyticAt ℂ (fun s ↦ Φ (-s)) s₀ := hΦan.comp hneg  have hmero1 : MeromorphicAt (fun w ↦ -deriv riemannZeta w / riemannZeta w) s₀ :=    (meromorphicAt_riemannZeta s₀).deriv.neg.div (meromorphicAt_riemannZeta s₀)  have h1 := neg_one_le_meromorphicOrderAt_neg_zeta_logDeriv s₀  have h2 : (0 : WithTop ℤ) ≤ meromorphicOrderAt (fun s ↦ Φ (-s)) s₀ :=    hΦneg_an.meromorphicOrderAt_nonneg  rw [show (fun s ↦ (-deriv riemannZeta s / riemannZeta s) * Φ (-s))      = (fun w ↦ -deriv riemannZeta w / riemannZeta w) * (fun s ↦ Φ (-s)) from rfl,    meromorphicOrderAt_mul hmero1 hΦneg_an.meromorphicAt]  calc ((-1 : ℤ) : WithTop ℤ) = ((-1 : ℤ) : WithTop ℤ) + 0 := by rw [add_zero]    _ ≤ _ := add_le_add h1 h2