Bernoulli polynomials

Stream: new members

[Gareth Ma]

Hi, I am working on Bernoulli polynomials, and in particular removing the TODO in the file. Does anyone know about any important theorems related to Bernoulli numbers or Bernoulli polynomials? I have also written a short outline on what I will prove: https://grhkm21.github.io/posts/bernoulli-polynomials/ (While writing I found that quite a few exists already, but not the main theorem) Since I know that these polynomials are used in interpolation theory quite a lot? But I know nothing about that

[Gareth Ma]

And yea I can formalise it probably tomorrow, I am going out tonight

[Gareth Ma]

5317B885-EA31-462A-AEB4-ED8F1CDD48C2.jpg

[Kevin Buzzard]

One cool result would be relating the special values of Riemann zeta at negative integers to Bernoulli numbers, but maybe we don't have Riemann zeta yet.

[Gareth Ma]

We indeed don’t have (analytic continuation of) Riemann zeta function, as far as I know? Otherwise things like PNT might be nice to work on

[Kevin Buzzard]

You might be interested to know that my PhD student Ashvni has proved that Bernoulli numbers are related to the special values of the p-adic zeta function in Lean :-) It was a long-term goal of mine to get the p-adic variant formalised before the classical version :-)

[Kevin Buzzard]

Another really nice TODO would be to work out the power series expansion of Eisenstein series. These are some of the simplest examples of modular forms, and their constant terms are related to Bernoulli numbers. However I suspect that any sensible way of doing this would involve going via the zeta function.

Oh! Do we have that the special values of zeta at positive even integers are related to Bernoulli numbers? I think Loeffler was working on this.

[David Loeffler]

Oh! Do we have that the special values of zeta at positive even integers are related to Bernoulli numbers? I think Loeffler was working on this.

Yes, we do, that's in mathlib now, see has_sum_zeta_nat

[David Loeffler]

(or has_sum_one_div_nat_pow_mul_fourier for a more general version relating values of Bernoulli polynomials on [0, 1] to Hurwitz zeta values)

[Kevin Buzzard]

Oh that is so cool! Do you think that the computation proving that E_k(z):=sum'_{a,b}(az+b)^{-k} is a constant times c+sum_n sigma_{k-1}(n)q^n for k>=4 even is within reach?

[David Loeffler]

I don't think the definition of the Eisenstein series has made it into mathlib yet, so I haven't tried to attack that. (@Chris Birkbeck What's the status on that?)

[Chris Birkbeck]

I've actually been thinking about the q-expansion for Eisenstein series this week. I think they are within reach. I going to see how far I can get before hitting an analytic wall

[David Loeffler]

As for the original question: I think nobody's done Euler--Maclaurin summation yet -- that's a nice application of Bernoulli polynomials.

[Chris Birkbeck]

I've started working on fixing up the Eisenstein series stuff for mathlib. But it'll take a while until it's added.

[Chris Birkbeck]

Kevin Buzzard said:

Oh that is so cool! Do you think that the computation proving that E_k(z):=sum'_{a,b}(az+b)^{-k} is a constant times c+sum_n sigma_{k-1}(n)q^n for k>=4 even is within reach?

Done!

[Kevin Buzzard]

In Lean 4? ;-)

[Chris Birkbeck]

Kevin Buzzard said:

In Lean 4? ;-)

stay tuned :)

[Ruben Van de Velde]

Chris Birkbeck said:

Kevin Buzzard said:

In Lean 4? ;-)

stay tuned :)

Btw, @Chris Birkbeck , I started looking at porting some of your modular forms works a while ago at https://github.com/CBirkbeck/ModularForms/compare/master...Ruben-VandeVelde:ModularForms:port?expand=1 , in case it's helpful

[Chris Birkbeck]

Ruben Van de Velde said:

Chris Birkbeck said:

Kevin Buzzard said:

In Lean 4? ;-)

stay tuned :)

Btw, Chris Birkbeck , I started looking at porting some of your modular forms works a while ago at https://github.com/CBirkbeck/ModularForms/compare/master...Ruben-VandeVelde:ModularForms:port?expand=1 , in case it's helpful

Oh this is great! Thank you, I will definitely make use of this

[Chris Birkbeck]

Kevin Buzzard said:

In Lean 4? ;-)

Ok its in lean 4 now :)

[Chris Birkbeck]

Ruben Van de Velde said:

Chris Birkbeck said:

Kevin Buzzard said:

In Lean 4? ;-)

stay tuned :)

Btw, Chris Birkbeck , I started looking at porting some of your modular forms works a while ago at https://github.com/CBirkbeck/ModularForms/compare/master...Ruben-VandeVelde:ModularForms:port?expand=1 , in case it's helpful

This was really helpful, thank you!