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 !