Defining the gamma function

Stream: general

[Hunter Monroe]

Could I get some guidance on defining the gamma function? It is either undefined at zero or infinite--how should that be handled? It is defined with an integral from zero to infinity--does Lean allow that?

[Hanting Zhang]

I think limits of interval integrals were defined awhile back by @Benjamin Davidson

[Hanting Zhang]

For some reason I can't seem to find it though

[Benjamin Davidson]

I think some of the integral stuff I added will help you with this, but I haven't done anything with improper integrals. You should see #7164 (cc @Anatole Dedecker )

[Scott Morrison]

It probably should be defined to be 0 (or perhaps 37...) at 0. It's essentially always best to make definitions total functions with garbage values at "undefined" points, and then put hypotheses into lemmas about the definition that avoid these cases so that the lemmas can be true.

[Hanting Zhang]

(deleted)

[Scott Morrison]

I don't think this is right. gamma z will always be an integral from 0 to infty. It's just that at z = 0 that integral doesn't converge.

[Scott Morrison]

Perhaps the integration set up is already designed to return zero in this case --- I don't have any experience with it.

[Benjamin Davidson]

What Scott is saying sounds more right to me

[Benjamin Davidson]

Ostensibly, gamma 0 would give you the integral of $x^{-1}exp(-x)dx$ from 0 to infinity , right?

[Hanting Zhang]

Oh my goodness I should really think about what I type more closely

[Hanting Zhang]

Thanks for catching that, sorry for the noise

[Scott Morrison]

No worries. :-) Just think of zulip as an initial stage of the typechecker verifying your theorems for you!

[Scott Morrison]

(We really should write the by zulip and by mario tactics someday. :-)

[Mario Carneiro]

Scott Morrison said:

Perhaps the integration set up is already designed to return zero in this case --- I don't have any experience with it.

:point_up: This. Integral is already totalized so it will already return 0 at non-convergent points. Not sure about the complex values though

[Sebastien Gouezel]

The definition with the integral will have a problem, though: the integral is not converging for z < 0, so one would also get the value 0 for z < 0. But this is not right: one should instead use the value of the meromorphic continuation at z, which happens to be real.

[Mario Carneiro]

I recall using a slightly more complex definition that converges everywhere in metamath

[Mario Carneiro]

http://us.metamath.org/mpeuni/df-lgam.html

[Mario Carneiro]

$\log\Gamma(z)=\sum_{m=1}^\infty(z\log(1+1/m)-\log(z/m+1))-\log z$

[Mario Carneiro]

It is nicer to define the logarithm of the gamma function first and then define $\Gamma(z)=\exp(\log \Gamma(z))$ because the log gamma function is not literally the log of the gamma function (it is one possible analytic choice of the branch cuts)

[Mario Carneiro]

Although I think this definition will not automatically give 0 at nonconvergent points (plus even if it did in the log-Gamma function, you would have to re-zero it when defining Gamma itself)

[Mario Carneiro]

Sebastien Gouezel said:

The definition with the integral will have a problem, though: the integral is not converging for z < 0, so one would also get the value 0 for z < 0. But this is not right: one should instead use the value of the meromorphic continuation at z, which happens to be real.

By the way, while I am familiar with this idea of "just analytically continue the function" from both the Gamma function and the zeta function, this sidesteps an important issue, which is why the analytic continuation exists and doesn't just crash and burn like in the j-invariant. I don't know any way to prove these functions have an analytic continuation besides using a separate formula that converges on the relevant domain, at which point you may as well use that as the definition.

[Kevin Buzzard]

For Riemann zeta, this is delicate. The zeta function is a global object and analytic continuation of global objects has content. An algebraic variety (e.g. the zero locus of a polynomial with rational coefficients) is a more general global object with a zeta function (defined as an infinite product, a generalisation of $\zeta(s)=\prod_p(1-p^{-s})^{-1}$ over primes $p$) and it is not known in general how to analytically continue it beyond the domain where the product converges; in general this is a big and difficult conjecture. The Riemann zeta function is zeta function of one point (i.e. the zero locus of $x=0$ in 1-space). For plane cubics e.g. the zero locus of $y^2=x^3+Ax+B$ in 2-space, the only known proof of analytic continuation goes via all the Taylor--Wiles FLT machinery).

But Gamma is a local object, so things are much easier. Meromorphic continuation for $\Gamma$ follows immediately from $\Gamma(z+1)=z\Gamma(z)$, or more precisely $\Gamma(z)=\Gamma(z+1)/z$, because if you've got $\Gamma(z)$ defined on $Re(s)>\sigma$ then the right hand side defines it for $Re(s)>\sigma-1$.

[Mario Carneiro]

I used a similar trick for the zeta function, with the definition

$$\xi(s)=\sum_{n=0}^\infty\frac{1}{2^{n+1}}\sum_{k=0}^n(-1)^k{n\choose k}(k+1)^s$$

and $\zeta(s)=\xi(s)/(1-2^{1-s})$. This definition still requires patching up some simple poles at the zeros of $1-2^{1-s}$ other than 1, but those can be simple extension by continuity since we're only filling in some discrete points.

[Mario Carneiro]

(That said, I never finished the proof that zeta, so defined, is in fact well defined and matches the usual sum definition where it converges, so this is more of a plan of action than a completed demonstration. I did manage to prove that the gamma function is uniformly continuous and satisfies the defining functional equation though.)

[Mario Carneiro]

As for generalizations (I guess these are L-functions?), I don't really understand what sort of convergence results and generalizations are worth exploring. I know the zeta function from the headlines and million dollar problems but I'm no number theorist

[Mario Carneiro]

That is, I imagine that a lot of work for the zeta function can be done in more generality and maybe that would be helpful if we want that generality in the future, but I know that there are more side conditions in the generalizations and I can't tell if it would be a lot harder to derive properties of the zeta function via its generalizations

[Kevin Buzzard]

Mathematically the things one could look at is: meromorphic continuation of zeta to the entire complex plane (accessible once we have the machinery), meromorphic continuation of Dirichlet L-functions $\sum_n\chi(n)/n^s$ with $\chi$ a periodic function from the naturals to the complexes (e.g. a Dirichlet character), and the most general "abelian" situation is meromorphic continuation of Hecke L-functions (this is the content of Tate's thesis and contour integrals are involved but not seriously). My impression is that Eberl has done all the Dirichlet stuff in Isabelle/HOL but nobody is close to Hecke L-functions. In the non-abelian global setting, a surprisingly easy result is analytic continuation of the L-function attached to a modular form, which would be something really cool to aim for and definitely within scope -- it's much easier than zeta. This is how you do L-functions (PS for me L-function and zeta-function are synonymous) of elliptic curves -- you prove they all come from modular forms (the hard part) and then analytically continue the modular form L-function, which equals the elliptic curve L-function (this is the definition of "comes from a modular form").

[Kevin Buzzard]

One thing which will be hard for us is proving that the space of modular forms is finite-dimensional; all the proofs of this I know involve things which are a long way from being in Lean. However I don't think one needs finite-dimensionality to prove meromorphic continuation of eigenforms; one just needs Hecke algebras. Someone expressed an interest in working on this with me over the summer, and also Chris Birkbeck is thinking about this stuff now, as is Heather. Analytic continuation of L-function of a modular form would be a neat goal, and as I say the analysis is easier than Riemann zeta.

[Mario Carneiro]

Analytic continuation of L-function of a modular form would be a neat goal

Do we even have modular forms or anything in the same ballpark? I've never seen this formalized so it's all greek to me, and it seems like the term means six different things and there is some deep theorem or other connecting them (Langlands program?).

I looked on wikipedia for generalizations of the Riemann zeta function and it mentions the Hurwitz zeta function, which seems to be a pretty straight generalization. The Dirichlet L-functions are apparently linear combinations of the Hurwitz zeta function (do you concur?), and the infinite series representation also generalizes (I like the series representation because it is very concrete).

[Anatole Dedecker]

Benjamin Davidson said:

I think some of the integral stuff I added will help you with this, but I haven't done anything with improper integrals. You should see #7164 (cc Anatole Dedecker )

To answer this : I don't think you will need any of my work to lay out the definition of the gamma function, because you can just write it as the Bochner integral over Ici 0. But you may need some of it to prove it converges, because my PR will allow to prove integrability of well known functions (I'm thinking of exp (-x), which you could easily prove integrable on Ici 0 using my work), and then use them as bounds whenever you need them.

[James Arthur]

Just to add to this I have also been working on the Gamma function. I was 'translating' the isabelle here into Lean. I didn't get very far though as I got distracted by some log stuff. As far as I remember, it goes via the log gamma series. I decided to try and stay clear of the integral stuff, and stay with the series. It involves a lot of convergence proofs but it seemed it was a nice enough route there.

[Hunter Monroe]

OK I will take no further action on the gamma function and let others implement this.

[Kevin Buzzard]

@Mario Carneiro I think modular forms are coming. The general rule with $L$-functions is that for a certain kind of sequence $a_1,a_2,a_3,\ldots$ (namely one "coming from arithmetic") it is sometimes worthwhile to consider $L(a,s)=\sum_{n\geq1}a_n/n^s$. If the sequence doesn't grow too quickly then the sum converges for real part of s suff large, and if the sequence really is arithmetic then the $L$-function should have a meromorphic continuation to the whole complex plane (this is philosophy, not mathematics). A modular form is a function on the upper half plane with a power series expansion $f(z)=\sum_{n\geq0}a_ne^{2\pi i n z}$ and if you forget $a_0$ then you get a sequence which is arithmetic because Ramanujan proved lots of wacky things about certain modular forms which number theorists are interested in. Yes, Hurwitz zeta functions and Dirichlet L-functions are related in a relatively straightforward manner. If $0<q=m/d\leq 1$ then $1/d^s$ times Hurwitz $\zeta(s,q)$ gives you the sequence defined by $a_n=1$ if $n$ is congruent to $m$ mod $d$ and 0 otherwise, so you can build any periodic sequences with these. Dirichlet $L$-functions are also L-functions coming from periodic sequences. Modular forms on the other hand don't give periodic sequences, for example you can define $a_n$ to be the number of ways that $n$ is the sum of two integer squares and that will be a modular form, although this statement has content (the content is essentially the assertion that the $L$-function has analytic continuation and functional equation).