Riemann zeta function

Stream: Is there code for X?

[Chris Birkbeck]

Has the Riemann zeta function been defined in lean? The "version" I am interested in is the infinite sum definition. I think I can see how one would define it using tsum but I have no idea really how to check its summable (even for large positive integer values).

[Yaël Dillies]

There has been recent discussions happening (and Kevin Buzzard can definitely tell you more): https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Defining.20the.20gamma.20function

[Chris Birkbeck]

Ah I missed this discussion, thank you!

[Kevin Buzzard]

@Chris Birkbeck Do you know @Jamie Bell ? He's a 1st year LSGNT student. He wrote tprod recently to define the L-function of an elliptic curve! To check it's summable I'd like to use the integral test. Do we have this in Lean?

[Chris Birkbeck]

@Kevin Buzzard Yes his work on L-functions. I saw the tprod and prodable definitions, but again, I'm not sure how to prove something is prodable. I wondered if maybe this had already been done for the Riemann zeta function as its so famous.

I'm not sure if the integral test is in lean, but that said, I'm still very bad at finding what is and isn't in lean.

[Kevin Buzzard]

As I have probably told you privately, if the analysts don't get their act together soon then thanks to Ashvni's work we run a very real risk of having the definition of the p-adic zeta function before we have the classical one :-)

[Chris Birkbeck]

People sometimes joke that we should learn p-adic analysis before real analysis, it sounds like this is actually happening in Lean!

[Kevin Buzzard]

It's because p-adic analysis is actually easier :p