Zeta functions

Stream: Is there code for X?

[Ashvni Narayanan]

Is anybody working on zeta functions?

[Aaron Anderson]

I've defined an arithmetic_function called zeta, but I don't know enough about the analysis library to define the corresponding L-function. Indeed, I'm not even sure if it can be defined in any satisfying way yet.

[Aaron Anderson]

I also believe @Alex Kontorovich was working on writing a statement of the Riemann hypothesis in lean, but I'm not sure how far that project has gotten.

[Alex Kontorovich]

That's right, Brandon Gomes and I formalized RH:

https://github.com/bhgomes/lean-riemann-hypothesis

But the formalization is not mathlib-appropriate; there are standalone files which contain the definitions etc of zeta (and Dirichlet eta) in which certain assumptions are made on the existence and properties of things like the exponential function and logs. Then there is a separate file which implements these things in Lean. It would be a good project to turn what we've done into something that can be incorporated into mathlib...

[Aaron Anderson]

I have made a start on defining L-series at branch#l_series.

[Aaron Anderson]

This is of course missing the analytic continuation part that @Alex Kontorovich did for the zeta function, and doesn't have any properties yet about the sums or products of L-series.

[Heather Macbeth]

@Aaron Anderson Is it perhaps worth defining the L-series as a formal power series, docs#power_series, and relying on @Yury G. Kudryashov's work in progress to convert that to an analytic funtion? Then the facts about convergence can be deduced from the general theory in docs#analytic_at

[Heather Macbeth]

At least, I think that's the general idea. I don't know how it's going to work in practice (Yury or @Sebastien Gouezel can probably comment), or how close Yury is to having the missing piece.

[Aaron Anderson]

I've thought about that a little bit, but I'm not sure there's one obvious way to do it, and I'm probably not the person to pick one way to do it out of several.

[Aaron Anderson]

For instance, defining it as the formal power series about z = 0 is not going to work, because the L-series we care the most about don't converge at 0

[Heather Macbeth]

I see ... the point is that it's not a power series, it's a different kind of series.

[Heather Macbeth]

I mean, it'll be a power series in neighbourhoods of various points, under the hood, because it's analytic, but it's not a priori defined as a power series.

[Heather Macbeth]

OK, here's a question: do L-series make sense in Banach algebras? :). If so, should one do the theory there?

[Aaron Anderson]

Does a Banach algebra A have has_pow N A?

[Alex Kontorovich]

The standard way to define a class of L-functions is to assume the coefficients grow at most polynomially, |a_n| \le C n^A. Then you have absolute convergence for Re(s)>A+1. This is implicit in the thing Brandon and I did; shouldn't be hard to implement (since it's basically there, just needs to be converted to mathlib format). At some point Brandon and I discussed doing the Selberg class, which I have some ideas on; would be great!... (Then we have the space of "all" L-functions, conjecturally...)

[Heather Macbeth]

Aaron Anderson said:

Does a Banach algebra A have has_pow N A?

We'll have the exponential in the Banach algebra (just like the matrix exponential, defined as a power series). I don't know if you can define logarithms? If you have both exponential and log, then you can take powers.

[Aaron Anderson]

Alex Kontorovich said:

The standard way to define a class of L-functions is to assume the coefficients grow at most polynomially, |a_n| \le C n^A. Then you have absolute convergence for Re(s)>A+1. This is implicit in the thing Brandon and I did; shouldn't be hard to implement (since it's basically there, just needs to be converted to mathlib format). At some point Brandon and I discussed doing the Selberg class, which I have some ideas on; would be great!... (Then we have the space of "all" L-functions, conjecturally...)

This sounds totally reasonable to me, and I replicated the A = 1 case in my code, mostly to try out the infinite sum library for myself.

[Aaron Anderson]

I think the question that @Heather Macbeth and I are both thinking about is whether there is a slick way to guarantee analyticity on the domain of convergence with the existing mathlib library for analytic functions, and unfortunately the only part of that library I have any awareness of is the part that has to do with formal power series.

[Heather Macbeth]

We'll need theorems like, locally uniform limits of sequences of analytic functions are analytic. (Alex and I were just discussing this the other day.)

[Aaron Anderson]

Yeah, I think we'll need a bunch of actual analysis to say that they're analytic...

[Aaron Anderson]

How much more work is necessary on this particular approach before it's worth PRing?

[Aaron Anderson]

I think for that we'd need to be at least somewhat confident that the correct way to define these is by first defining the possibly-convergent infinite sums as nat.arithmetic_function.l_series and then later to come in and define nat.arithmetic_function.l_function as an analytic continuation somehow.

[Aaron Anderson]

Also I should probably add scalar multiplication, addition and multiplication rules. The scalar multiplication and addition rules will be simple enough, but l_series won't be a linear map because of convergence questions.

[Aaron Anderson]

The multiplication might need quite a bit of additional infinite sum lemmas, so that might even be more like a second PR, if people think the rest is worth PRing as is.

[Kevin Buzzard]

The theory of Dirichlet series is done in rather large generality in Chapter 6 of Serre's Course in Arithmetic

[Kevin Buzzard]

As Heather says, you need that locally uniform limits of holomorphic functions are holomorphic (and that the derivatives tend locally uniformly to the derivative). There are also some comments about how it's all a special case of the Laplace transform of a measure (in this case a discrete measure). Serre shows (it's slightly delicate) that if a Dirichlet series converges at z0 then it converges for all z with Re(z)>Re(z0). He then shows that the Dirichlet series associated to a strictly multiplicative function has an infinite product expansion. He then embarks on the slightly delicate proof that there are infinitely many primes in an AP.

[Kevin Buzzard]

Then in chapter 7 he starts on modular forms :heart: :heart: