Residue of the Riemann zeta function

Stream: Is there code for X?

[Michael Stoll]

Do we have the fact that $\lim_{s \to 1} (s-1) \zeta(s) = 1$ (where $\zeta$ is the Riemann zeta function)?
Looking through NumberTheory.ZetaFunction, it does not look like it is there (at least not in this form), but maybe it can be deduced easily from what exists? @David Loeffler

[David Loeffler]

Michael Stoll said:

Do we have the fact that $\lim_{s \to 1} (s-1) \zeta(s) = 1$ (where $\zeta$ is the Riemann zeta function)?
Looking through NumberTheory.ZetaFunction, it does not look like it is there (at least not in this form), but maybe it can be deduced easily from what exists? David Loeffler

Yes, we have that $\Lambda(s) - 1/s - 1/(s - 1)$ is entire (+ in particular holomorphic at $s = 1$) so the calculation of the residue is easy to get from that. (edit: formatting)

[Michael Stoll]

OK; which lemma is that precisely?

[Eric Rodriguez]

docs#differentiable_completed_zeta₀

[David Loeffler]

The linkifier seems to have got confused by the subscript 0, here's a hand-rolled link: differentiable_completed_zeta₀

[Michael Stoll]

Seems I overlooked that when looking through the file.
I'll try that approach later. (Yesterday I produced a long and ugly proof (modulo two minor sorries) using the functional equation for the zeta function. It will be interesting to see if using the completed zeta function leads to a shorter/less ugly proof...)

[David Loeffler]

How does the following compare for shortness / ugliness with your previous proof?

import Mathlib

open Set Filter Topology

lemma ZetaLimit1 : Tendsto (fun s ↦ (s - 1) * riemannCompletedZeta s) (𝓝[≠] 1) (𝓝 1) := by
  unfold riemannCompletedZeta
  simp_rw [mul_add, mul_sub, (by simp : 𝓝 (1 : ℂ) = 𝓝 (0 - 0 + 1))]
  refine (Tendsto.sub ?_ ?_).add ?_
  · rw [(by simp : 𝓝 (0 : ℂ) = 𝓝 ((1 - 1) * riemannCompletedZeta₀ 1))]
    refine (Continuous.tendsto ?_ _).mono_left nhdsWithin_le_nhds
    exact Continuous.mul (by continuity) differentiable_completed_zeta₀.continuous
  · rw [(by simp : 𝓝 (0 : ℂ) = 𝓝 ((1 - 1)  * (1 / 1)))]
    refine (ContinuousAt.tendsto ?_).mono_left nhdsWithin_le_nhds
    exact ((continuous_sub_right _).continuousAt).mul <|
      continuousAt_const.div continuousAt_id one_ne_zero
  · simp_rw [mul_one_div]
    refine (tendsto_const_nhds.mono_left nhdsWithin_le_nhds).congr' ?_
    refine eventually_nhdsWithin_of_forall (fun s hs ↦ ?_)
    dsimp only
    rw [div_self]
    simpa [sub_eq_zero] using Set.mem_compl_singleton_iff.mpr hs

lemma ZetaLimit2 : Tendsto (fun s ↦ (s - 1) * riemannZeta s) (𝓝[≠] 1) (𝓝 1) := by
  suffices : Tendsto (fun s => (s - 1) *
      (↑Real.pi ^ (s / 2) * riemannCompletedZeta s / Complex.Gamma (s / 2))) (𝓝[≠] 1) (𝓝 1)
  · apply this.congr'
    refine (eventually_ne_nhdsWithin (one_ne_zero' ℂ)).mp (eventually_of_forall ?_)
    intro x hx
    simp [riemannZeta_def, Function.update_noteq hx]
  have h0 : Tendsto (fun s : ℂ ↦ (Real.pi : ℂ)^ (s / 2 : ℂ)) (𝓝[≠] 1) (𝓝 (↑Real.pi ^ (1 / 2 : ℂ)))
  · refine ((continuousAt_id.div_const _).const_cpow ?_).tendsto.mono_left nhdsWithin_le_nhds
    exact Or.inl <| Complex.ofReal_ne_zero.mpr Real.pi_ne_zero
  have h1 : Tendsto (fun s ↦ 1 / Complex.Gamma (s / 2)) (𝓝[≠] 1) (𝓝 (1 / ↑Real.pi ^ (1 / 2 : ℂ)))
  · rw [← Complex.Gamma_one_half_eq]
    refine (Continuous.tendsto ?_ _).mono_left nhdsWithin_le_nhds
    simp_rw [one_div]
    exact (Complex.differentiable_one_div_Gamma).continuous.comp (continuous_id.div_const _)
  convert (ZetaLimit1.mul h0).mul h1 using 1
  · ext1 s
    ring
  · rw [one_mul, mul_one_div, div_self]
    rw [(by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)), ← Complex.ofReal_cpow Real.pi_pos.le, Ne.def,
      Complex.ofReal_eq_zero, Real.rpow_eq_zero_iff_of_nonneg Real.pi_pos.le]
    exact fun h ↦ Real.pi_pos.ne' h.1

[Michael Stoll]

It uses many of the same (or similar) ingredients, unsurprisingly, but is certainly a bit better than what I had (which can ceertainly be improved a bit). Thanks!

[David Loeffler]

You're welcome! Are you going to PR this as part of your Euler products project, or shall I PR it separately?

[Michael Stoll]

You are certainly welcome to PR this. At this point, I'm targetting estimates for the complex log (in the open disk of radius 1 about 1) with my PRs; I don't need the residue computation in Matlib urgently. But it should definitely be available!