Zulip Chat Archive

Stream: Is there code for X?

Topic: Zeta functions


view this post on Zulip Ashvni Narayanan (Nov 23 2020 at 14:02):

Is anybody working on zeta functions?

view this post on Zulip Aaron Anderson (Nov 23 2020 at 19:32):

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.

view this post on Zulip Aaron Anderson (Nov 23 2020 at 19:35):

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.

view this post on Zulip Alex Kontorovich (Nov 23 2020 at 20:57):

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...

view this post on Zulip Aaron Anderson (Jan 13 2021 at 17:24):

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

view this post on Zulip Aaron Anderson (Jan 13 2021 at 17:25):

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.

view this post on Zulip Heather Macbeth (Jan 13 2021 at 21:33):

@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

view this post on Zulip Heather Macbeth (Jan 13 2021 at 21:34):

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.

view this post on Zulip Aaron Anderson (Jan 13 2021 at 21:39):

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.

view this post on Zulip Aaron Anderson (Jan 13 2021 at 21:40):

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

view this post on Zulip Heather Macbeth (Jan 13 2021 at 21:42):

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

view this post on Zulip Heather Macbeth (Jan 13 2021 at 21:43):

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.

view this post on Zulip Heather Macbeth (Jan 13 2021 at 21:46):

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

view this post on Zulip Aaron Anderson (Jan 13 2021 at 21:47):

Does a Banach algebra A have has_pow N A?

view this post on Zulip Alex Kontorovich (Jan 13 2021 at 21:47):

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...)

view this post on Zulip Heather Macbeth (Jan 13 2021 at 21:48):

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.

view this post on Zulip Aaron Anderson (Jan 13 2021 at 21:50):

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.

view this post on Zulip Aaron Anderson (Jan 13 2021 at 21:51):

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.

view this post on Zulip Heather Macbeth (Jan 13 2021 at 21:52):

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.)

view this post on Zulip Aaron Anderson (Jan 13 2021 at 22:05):

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

view this post on Zulip Aaron Anderson (Jan 13 2021 at 22:05):

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

view this post on Zulip Aaron Anderson (Jan 13 2021 at 22:06):

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.

view this post on Zulip Aaron Anderson (Jan 13 2021 at 22:08):

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.

view this post on Zulip Aaron Anderson (Jan 13 2021 at 22:09):

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.

view this post on Zulip Kevin Buzzard (Jan 13 2021 at 22:09):

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

view this post on Zulip Kevin Buzzard (Jan 13 2021 at 22:16):

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.

view this post on Zulip Kevin Buzzard (Jan 13 2021 at 22:16):

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


Last updated: May 17 2021 at 15:13 UTC