Riemann zeta

Stream: maths

[David Loeffler]

I have just completed the formalisation of the analytic continuation and functional equation of Riemann zeta, in the following form:

There exists a function ξ : ℂ → ℂ (the Landau–Riemann xi function) such that:

• ξ is holomorphic everywhere,
• for 1 < re s we have $\xi(s) = \tfrac{1}{2}s (s-1)\pi^{-s/2} \Gamma(s / 2) \sum_{n \in \mathbb{N}} \frac{1}{(n + 1)^s}$,
• for all s we have ξ(1 - s) = ξ(s).

The proof is about 800 lines of lean3 code.

[Ruben Van de Velde]

Planning to submit it to mathlib before we're done porting? :)

[Kevin Buzzard]

Congratulations! Do you have further plans? For example nonvanishing on Re(s)=1, generalisation to Dirichlet L-functions etc?

[Johan Commelin]

Congratulations with this milestone!

[David Loeffler]

Ruben Van de Velde said:

Planning to submit it to mathlib before we're done porting? :)

I'm currently drip-feeding bits of it into mathlib3, and making companion mathlib4 PR's for the parts which touch already-ported files. At some point I'll switch over to making mathlib4 PR's, but given that this proof depends on virtually the entire analysis library (measure theory, integration, Fourier analysis, Poisson summation...), that's not going to be any time soon.

[David Loeffler]

Kevin Buzzard said:

Congratulations! Do you have further plans? For example nonvanishing on Re(s)=1, generalisation to Dirichlet L-functions etc?

I am definitely planning to extend the result to cover general Dirichlet characters (in parallel with the process of splitting the proof into PR'able chunks).

[Filippo A. E. Nuccio]

Congratulations @David Loeffler !

[Newell Jensen]

I was looking to see if this was in mathlib4 yet but it doesn't seem to be. Any plans to still get this in by chance @David Loeffler ? I have been out of the lean loop for a bit (so rusty) but would be willing to try and help get this ported if that would help at all.

[David Loeffler]

See https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/LSeries/RiemannZeta.html#Definition-of-the-Riemann-zeta-function

[David Loeffler]

It's not quite literally true that everything from my 2023.03.29 post is in mathlib, because in the end I went for a formulation in terms of $\Lambda_0(s) = \Lambda(s) + \frac{1}{s} + \frac{1}{1-s}$, rather than $\xi(s) = s (s - 1) \Lambda(s)$. But it is clearly equivalent.

All the above is also available for general Dirichlet characters too, including the nonvanishing on Re(s) = 1 which was a joint project with Michael Stoll.

[Newell Jensen]

I did briefly see that but will take a closer look. Thanks for contributing this.