Source indexedtheorem · leanprover/lean4:v4.32.0

meromorphicOrderAt_riemannZeta_one

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:106 to 118

Source documentation

The Riemann zeta function has a simple pole at s = 1: its meromorphic order there is -1.

Exact Lean statement

theorem meromorphicOrderAt_riemannZeta_one : meromorphicOrderAt riemannZeta 1 = (-1 : ℤ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem meromorphicOrderAt_riemannZeta_one : meromorphicOrderAt riemannZeta 1 = (-1 : ℤ) := by  have hsub : MeromorphicAt (fun s : ℂ ↦ s - 1) 1 :=    (analyticAt_id.sub analyticAt_const).meromorphicAt  have h0 : meromorphicOrderAt ((fun s : ℂ ↦ s - 1) * riemannZeta) 1 = 0 :=    (tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero      (hsub.mul (meromorphicAt_riemannZeta 1))).1 ⟨1, one_ne_zero, riemannZeta_residue_one⟩  rw [meromorphicOrderAt_mul hsub (meromorphicAt_riemannZeta 1),    meromorphicOrderAt_id_sub_const] at h0  obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.1 (meromorphicOrderAt_riemannZeta_ne_top 1)  rw [← hn] at h0 ⊢  have hni : (1 : ℤ) + n = 0 := by exact_mod_cast h0  norm_cast  omega