Source indexedtheorem · leanprover/lean4:v4.32.0

eq12_meromorphicOrderAt_nonneg_of_ne

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:447 to 459

Source documentation

At a point of the box where ζ ≠ 0 and s ≠ 1, the eq.(12) integrand is analytic, so its meromorphic order is non-negative (no pole).

Exact Lean statement

theorem eq12_meromorphicOrderAt_nonneg_of_ne {Φ : ℂ → ℂ} {b : ℝ}
    (hΦ : AnalyticOnNhd ℂ Φ {s : ℂ | -(1 + b) < s.re ∧ s.re < b})
    {a T : ℝ} (ha : 0 < a) (hab : a < b) {s : ℂ}
    (hsbox : s ∈ Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I))
    (hζ_ne : riemannZeta s ≠ 0) (hs1 : s ≠ 1) :
    0 ≤ meromorphicOrderAt (fun s ↦ (-deriv riemannZeta s / riemannZeta s) * Φ (-s)) s

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem eq12_meromorphicOrderAt_nonneg_of_ne {Φ : ℂ → ℂ} {b : ℝ}    (hΦ : AnalyticOnNhd ℂ Φ {s : ℂ | -(1 + b) < s.re ∧ s.re < b})    {a T : ℝ} (ha : 0 < a) (hab : a < b) {s : ℂ}    (hsbox : s ∈ Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I))    (hζ_ne : riemannZeta s ≠ 0) (hs1 : s ≠ 1) :    0 ≤ meromorphicOrderAt (fun s ↦ (-deriv riemannZeta s / riemannZeta s) * Φ (-s)) s := by  have hζ_an : AnalyticAt ℂ riemannZeta s :=    analyticOn_riemannZeta s (Set.mem_compl_singleton_iff.mpr hs1)  have hlog_an : AnalyticAt ℂ (fun w ↦ -deriv riemannZeta w / riemannZeta w) s :=    (hζ_an.deriv.neg).div hζ_an hζ_ne  have hΦneg_an : AnalyticAt ℂ (fun s ↦ Φ (-s)) s :=    (hΦ (-s) (eq12_neg_mem_strip ha hab hsbox)).comp analyticAt_id.neg  exact (hlog_an.mul hΦneg_an).meromorphicOrderAt_nonneg