Source indexedtheorem · leanprover/lean4:v4.32.0

residue_neg_zeta_logDeriv_mul

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:380 to 387

Source documentation

Residue value (Part 4, with the analytic cofactor Φ(-·)): the residue of s ↦ (-ζ'/ζ)(s)·Φ(-s) at p equals -order(ζ, p)·Φ(-p).

Exact Lean statement

theorem residue_neg_zeta_logDeriv_mul {p : ℂ} {m : ℤ} {Φ : ℂ → ℂ}
    (hm : meromorphicOrderAt riemannZeta p = m) (hΦ : ContinuousAt Φ (-p)) :
    residue (fun s ↦ (-deriv riemannZeta s / riemannZeta s) * Φ (-s)) p = -(m : ℂ) * Φ (-p)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem residue_neg_zeta_logDeriv_mul {p : ℂ} {m : ℤ} {Φ : ℂ → ℂ}    (hm : meromorphicOrderAt riemannZeta p = m) (hΦ : ContinuousAt Φ (-p)) :    residue (fun s ↦ (-deriv riemannZeta s / riemannZeta s) * Φ (-s)) p = -(m : ℂ) * Φ (-p) := by  apply residue_eq_of_tendsto  have hΦt : Tendsto (fun z ↦ Φ (-z)) (𝓝[≠] p) (𝓝 (Φ (-p))) :=    (hΦ.comp continuous_neg.continuousAt).tendsto.mono_left nhdsWithin_le_nhds  refine ((tendsto_sub_mul_neg_zeta_logDeriv hm).mul hΦt).congr (fun z ↦ ?_)  ring