Basel problem / ζ(2)

Stream: maths

[Moritz Doll]

I would like to know whether anyone works on proving that $ζ(2) = \frac{π^2}{6}$ using Parseval's identity. I proposed this as a project for an intern of mine. I guess the mathlib version would be to calculate the zeta function for all even natural numbers, so the student project is of independent interest.

[Johan Commelin]

Mathlib doesn't even have a definition of $\zeta$ at the moment, does it? I'm not aware of anyone working on $\zeta(2) = \pi^2/6$.

[Moritz Doll]

Well $ζ(2) = \sum_{k=1}^{\infty} \frac{1}{k^2}$ and I was just too lazy to write the RHS.

[Johan Commelin]

Fair enough. Maybe it exists somewhere in arithmetic_function?

[Johan Commelin]

docs#nat.arithmetic_function.zeta

[Yaël Dillies]

I'm not aware of anyone working on $\zeta(2) = \pi$.

I hope nobody is working on that!

[Moritz Doll]

analysis.fourier is imported nowhere, so there might be another proof, but not the one I have in mind

[Riccardo Brasca]

@Marc Masdeu proved it I think, but maybe it is not in mathlib

[Riccardo Brasca]

https://github.com/mmasdeu/euler

[Marc Masdeu]

I followed a proof that used some recurrences for integrals of trig functions, but didn't generalize to $\zeta(2n)$. Maybe it should be in mathlib, but I got distracted by other things. My opinion is that the one that should be in mathlib is the formula for $\zeta(2n)$, together with all the necessary lemmas about Bernoulli numbers.

[David Loeffler]

I have posted a PR #14701 which evaluates ζ(2k) for all k using Parseval's theorem. It's a bit on the rough side at present, but it's a complete proof. I'm working on converting it into digestible chunks for review (the first two instalments have already been reviewed).

[Patrick Massot]

Analytic number theory is on fire tonight!

[David Loeffler]

(I'm curious what the octopus emoji means?)

[Patrick Massot]

The octopus is meant to be celebrating something (at least in most emoji fonts it looks cheerful and raises two tentacles in the air).

[Moritz Doll]

David Loeffler said:

I have posted a PR #14701 which evaluates ζ(2k) for all k using Parseval's theorem. It's a bit on the rough side at present, but it's a complete proof. I'm working on converting it into digestible chunks for review (the first two instalments have already been reviewed).

Sorry, but it would have been nice if you had said that you are working on this.

[David Loeffler]

I didn't see this Zulip thread until too late, sadly.

[David Loeffler]

Actually this was a "side-effect" of another project: my longer-term goal is to prove the functional equation relating ζ(1-s) and ζ(s), going via Poisson summation and the modularity of the Jacobi half-integer-weight theta series (i.e. pretty much Riemann's original proof -- there are alternative shorter proofs using contour integration but those are harder to formalise with the current state of the library). So that was why I got involved in overhauling analysis.fourier; evaluating critical values of zeta wasn't the primary goal.