holomorphic functions on the upper half plane

Stream: Is there code for X?

[Kevin Buzzard]

I remember back in 2018 Johan knocked off the definition of a modular form just to show it could be done. I don't even remember where this code is any more. Someone at Imperial has expressed interest in developing the theory a bit. I think finite-dimensionality of the spaces is out of reach right now, one proof I know uses facts about compact Riemann surfaces and the other uses contour integration, and both seem a fair way away right now (the student would be doing the project perhaps this term or next term). However even though we don't have finite-dimensionality, there are still plenty of things one could do, e.g. defining Hecke operators, and perhaps giving a non-constant example (one would need to be able show that things like $\sum_{a,b\in\mathbb{Z}^2-\{(0,0)\}}(a+bz)^{-4}$ is holomorphic in $z$, for $z$ complex with positive imaginary part).

A modular form is a holomorphic function on the upper half plane $\{z\in\mathbb{C}\,|\,Im(z)>0\}$, satisfying two axioms (a boundedness condition and a symmetry condition for a discrete group action), The first question I run into is how to do holomorphic functions on the upper half plane. Should this be a subtype? A complex manifold? Do we have the concept of a holomorphic function on an open subset of $\mathbb{C}$?

[Johan Commelin]

It's in your "Kevin turns 50" repository!

[Kevin Buzzard]

Oh yeah!

[Johan Commelin]

Finite dimensionality is an easy application of the theory of liquid $\mathbb R$-modules...

[Kevin Buzzard]

So here is a definition of a holomorphic function. Is this still state of the art? Or did we do some more analysis since 2018?

[Johan Commelin]

I think most of it is out of date; a lot of analysis was added since that repo

[Kevin Buzzard]

Indeed :-) This is why I am asking for advice about how to say "f is holomorphic" in 2021 (and also how to say "upper half plane"). Once I know that, I think we can get started (following your 2018 work!)

[Johan Commelin]

Can't we just say that f is differentiable over complex?

[Johan Commelin]

@Sebastien Gouezel @Heather Macbeth will know better how to deal with the upper half plane, I guess.

[Sebastien Gouezel]

You can consider a function from $\mathbb{C}$ to $\mathbb{C}$ which is differentiable (over the complexes) on the upper half-plane, seen as an open subset of the complex plane. It works, but you get a bunch of junk from the values on the complement of the upper half-plane (in particular, you will lose finite-dimensionality!) Another way is to consider the functions defined on the subtype. Open subsets of a manifold automatically get a manifold structure, so the upper half space already has the structure of a complex manifold, and it makes sense to talk about differentiable functions (over the complexes) on it.

[Heather Macbeth]

@Alex Kontorovich @Marc Masdeu (and I) have been trying this, actually. The definition of the modular group is done, so is its action on the upper half-plane. Next up is the fundamental domain.

[Sebastien Gouezel]

Did you go for the general manifold definition, or something more specific?

[Heather Macbeth]

We didn't really need to decide yet, because so far there's just stuff about a group action, nothing about functions which are preserved by it.

[Heather Macbeth]

It looks like

notation `SL(` n `,` R `)`:= special_linear_group (fin n) R

def H : set ℂ := { z | 0 < z.im }

instance SL2Z_action : mul_action SL(2, ℤ) H :=

[Heather Macbeth]

I was thinking that it would be easier to work with functions on ℂ with junk values, but it's not too late to go the manifold path. For me the bigger question (which Kevin already raised) is about how holomorphic functions are going to work:

Someday, and maybe not too far away, we will have a proof that analytic is the same as complex-differentiable. Which will be the primary object in mathlib's complex analysis library? That is, do we work with analytic functions and occasionally drop to complex-differentiability within certain proofs when convenient, or work with complex-differentiable functions and occasionally invoke the analyticity within certain proofs as needed?

[Sebastien Gouezel]

That's a good question. For now, the analytic groupoid is not defined in mathlib, so there is only one way to go, but in the future we will have to make a choice. Using analytic functions feels more natural to me, but it's just a feeling.

[Heather Macbeth]

While we're on the subject, I checked the Cauchy-Riemann equations a couple of months ago.
branch#complex-diff

I didn't PR it yet because it's not clear yet what the best formulation is to play well with Yury's version of Stokes' theorem (branch#measure-subadditive)

[Kevin Buzzard]

Oh that's great if there are people already working on it! I guess there are a few things in my head about modular forms, I'm sure we can find some other modular formy stuff to do, or some other way my student can get involved.