Principle branch of log gamma

Stream: Is there code for X?

[Geoffrey Irving]

Do we have the principle branch of log (gamma z) as a definition analytic off the negative real axis? Complex.log (Complex.Gamma z) isn't it since the principle branch of log gamma gets to wrap around a bunch.

I think the answer is no based on simple searches, but want to confirm.

[Geoffrey Irving]

One common definition (from Wikipedia, or Hare, Computing the Principal Branch of log-Gamma):
logGamma.png

[Sébastien Gouëzel]

I don't think we have it. There was some work on taking primitives of holomorphic functions on star-shaped domains (I don't think we have a suitable notion of simply connected domain yet, which is a shame), which would give it readily, but I don't think this has been merged into mathlib. @Vincent Beffara or @Alex Kontorovich might know better.

[Geoffrey Irving]

Yeah, when I was doing analytic continuation for Mandelbrot stuff I went the lazy route and used convex domains.

[Vincent Beffara]

I have code for primitives on star-shaped domains here: https://github.com/vbeffara/Curvint/blob/main/Curvint/Primitive.lean but it's a bit messy. In the same repo there is a construction of C0 contour integrals by lifting but that is beyond messy, I'm slowly working on it and eventually I believe it's the right thing to do but it will take a while.