Modular forms and related things

Stream: maths

[Chris Birkbeck]

So I think its time I start trying to get some of the modular forms code and related things PR'd. The issue is that I have several files with lots of dependencies, so what is the best thing to do? Should each file be a separate PR?

I've made a draft PR here https://github.com/leanprover-community/mathlib/pull/8979, so any advice on how to split things is welcome.

It basically contains the definitions of modular forms, a definition of holomorphic functions, and facts about SL(2,Z) , including that it is generated by two well-known matrices "S" and "T". (There are also things like the Weierstrass M-test and a definition of the Riemann zeta function (for real values), but these should be easier to split off).

[Ruben Van de Velde]

Is #8611 related?

[Kevin Buzzard]

A PR should be a couple of hundred lines at most, really, so even some of those single files are too long for one PR. It will be a lot of effort getting this stuff into mathlib (but this effort should be undertaken!).

[Chris Birkbeck]

Ruben Van de Velde said:

Is #8611 related?

Yes I used some of the definitions from here! But also extended some of the things in this PR.
Edit: or at least I used things from a recent PR related to this

[Kevin Buzzard]

Maybe you could start with a general_linear_group.lean PR and/or a Weierstrass M test PR?

[Kevin Buzzard]

Note that making a PR is hard work and takes some time. Do you already have push access to non-master branches of mathlib?

[Chris Birkbeck]

Yeah the general_linear_group is on the way.

[Chris Birkbeck]

and yes the M-test should be fine on its own. The issue is where there are several things with dependencies. I guess if you're saying each PR should only be a couple of hundred lines then that tells me what to do.

[Chris Birkbeck]

Kevin Buzzard said:

Note that making a PR is hard work and takes some time. Do you already have push access to non-master branches of mathlib?

yes

[Kevin Buzzard]

Other relatively straightforward things to do could be to PR short lemmas which you needed and which weren't in the API already (i.e. a PR with just one lemma in), e.g. the lemmas at the start of SL2Z_generators.lean shouldn't be in that file (and could well be in mathlib already, but if they're not then they could be made into a PR to data.int.basic and other appropriate places)

[Riccardo Brasca]

What is the consensus about holomorphic functions? Holomorphic on open subset of C is general enough? I think we really need to have complex_analysis.lean in mathlib...

[Kevin Buzzard]

Well the upper half plane is now a type of its own!

[Sebastien Gouezel]

We already have analytic functions.

[Chris Birkbeck]

Riccardo Brasca said:

What is the consensus about holomorphic functions? Holomorphic on open subset of C is general enough? I think we really need to have complex_analysis.lean in mathlib...

Yeah I don't really feel qualified to make the holomorphic definition, but I needed it so just went with that for now. Not that I can prove anything is holomorphic, so can definitely change once someone with more authority makes the correct definition

[Riccardo Brasca]

I have to catch up what happened in mathlib in the last month, but I am pretty sure we don't want to develop complex analysis for holomorphic functions over H, or C or whatever, but at least over any open subset of C

[Chris Birkbeck]

Sebastien Gouezel said:

We already have analytic functions.

Yes I think this is what I should use instead. I did have some issues in that lots of things wanted my maps to be from C to C and not from an open subset to C so the extend_by_zero was a hack from Kevins birthday repo that I used.

[Heather Macbeth]

Looking at Chris' code, I begin to think mathlib is missing some theory on (local) uniform convergence. We have the definitions docs#tendsto_uniformly_on, docs#tendsto_locally_uniformly_on, but it would be nice to have topological_space instances on α → β such that these definitions are precisely filter.tendsto for those topologies.

[Heather Macbeth]

There also seems to be glue missing between docs#tendsto_uniformly_on and docs#bounded_continuous_function

[Heather Macbeth]

With those in place, you have the Weierstrass M-test as docs#summable_of_norm_bounded.

[Oliver Nash]

Heather Macbeth said:

Looking at Chris' code, I begin to think mathlib is missing some theory on (local) uniform convergence. We have the definitions docs#tendsto_uniformly_on, docs#tendsto_locally_uniformly_on, but it would be nice to have topological_space instances on α → β such that these definitions are precisely filter.tendsto for those topologies.

Possibly related: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Metrisability.20of.20compact-open.20topology/near/251696483

[Chris Birkbeck]

Heather Macbeth said:

With those in place, you have the Weierstrass M-test as docs#summable_of_norm_bounded.

Yes I must admit, you mentioned proving it this way but I haven't had the chance to think about it this way. I PR'd the version I have, but do you think proving it this way would be better?

[Heather Macbeth]

@Oliver Nash Indeed it seems quite closely related. Will continue the discussion over there ...

[Chris Birkbeck]

So I'm a bit lost as to what to do about the complex holomorphic definition. Originally I used this

def is_holomorphic_on {D : open_subs} (f : D.1 → ℂ) : Prop := ∀ z : D.1, ∃ f', has_deriv_within_at (extend_by_zero f) (f') D.1 z

as my definition, which I can prove forms ring. There is also enough in mathlib to prove

lemma is_holomorphic_on_iff_differentiable_on (D : open_subs) (f : D.1 → ℂ): differentiable_on ℂ (extend_by_zero f) D.1 ↔ is_holomorphic_on f:=

Now, as far as I can tell we don't have an analytic_on definition, but we do have analytic_at, so the extension wouldn't be an issue. The issue is as far as I can see, we don't have a result (or at least I can't find) that says the product of two analytic functions is analytic. So I guess these things would need to be added.

I guess all of these definitions also have the slight annoyance that if one wants functions only defined on some open subset, then we need to use an extend_by_zero or similar, since as far as I can see all of these definitions are for functions between normed vector spaces. Is there a better way around this?

So there seem to be three possibilities for complex holomorphic functions, so my question is what should I use? are we close enough to having the necessary machinery for proving that they are all equivalent and therefore it makes no difference?

[Heather Macbeth]

@Chris Birkbeck Isn't this a bit of a moot point? We don't have the tools yet to prove the functions you're interested in are holomorphic, right? (You're interested in the Eisenstein series for the modular group, and in the Riemann zeta function, and if I understand correctly both of these require the theorem that a uniform limit of holomorphic functions is holomorphic.)

[Heather Macbeth]

I think that differentiable_on or mdifferentiable_on are the definitions for which we are most likely, soon-ish, to be able to prove that a uniform limit of holomorphic functions is holomorphic. (This is via Yury's WIP on Stokes.)

[Heather Macbeth]

So you could either work with functions f : ℂ → ℂ which are differentiable_on D, or with functions f : ℍ → ℂ which are mdifferentiable.

[Chris Birkbeck]

Ah so you're saying I should just wait until we have have the uniform limit of holo is holo proven and then go with that definition of holomorphic? I guess that is very reasonable.

[Chris Birkbeck]

Can on do differentiable_on D? I thought the D would have to be a normed vector space

[Heather Macbeth]

No, here ℂ is the normed vector space, so you consider functions on ℂ which are differentiable_on D (and just consider the values outside D as junk values).

[Chris Birkbeck]

Aha I get you, this is what I was doing with the extend_by_zero.

[Heather Macbeth]

Right, but don't literally extend by zero, instead just start with a function on the whole of ℂ.

[Chris Birkbeck]

Hmm but is that what we want? I only want to define modular forms on the upper half plane, so maybe using mdifferentiable is better (if it lets you work with f : ℍ → ℂ).

[Chris Birkbeck]

tbh I didn't know about mdifferentiable_on until now, but looking at it quickly it might be the best choice.

[Chris Birkbeck]

Chris Birkbeck said:

Hmm but is that what we want? I only want to define modular forms on the upper half plane, so maybe using mdifferentiable is better (if it lets you work with f : ℍ → ℂ).

btw this is just a personal preference, it would just feel weird having modular forms defined on the complex plane who satisfy some tranformation property on ℍ , it seems this would get messy

[Heather Macbeth]

To use mdifferentiable you will need to establish that the upper half-plane is a manifold. But this is not very difficult. Use docs#topological_space.opens.smooth_manifold_with_corners probably.

[Heather Macbeth]

@Chris Birkbeck Here's how I would set up the Eisenstein series construction. Following mathlib standard notation, denote by C(ℍ, ℂ) the space of continuous functions on the upper half-plane, equipped with the compact-open topology (i.e., the topology of locally uniform convergence). For now you would just like to construct $G_{2k}$ as an element of C(ℍ, ℂ), although eventually (when more complex analysis is available in mathlib) you will want to prove it is holomorphic.

Let's slightly modify what you wrote in your file and start by defining

def Eise (k : ℤ) (x : ℤ × ℤ) : C(ℍ, ℂ) :=
⟨λ z, 1/(x.1*z+x.2)^k, ... proof of continuity ...⟩

You want to prove ∀ k, summable (Eise k), i.e. that for each k the Eisenstein series is summable locally uniformly.

It will turn out that there is a family of seminorms on C(ℍ, ℂ), parametrized by the compact subsets s of ℍ, which induce topologies uniform_on ℂ s on C(ℍ, ℂ) (the topologies of uniform convergence on the s), with the following property:

lemma summable_compact_open_iff_forall [locally_compact_space α] [t2_space β] {ι : Type*}
  [decidable_eq ι] [nonempty ι] {l : filter ι} (F : ι → C(α, β)) :
  summable F
  ↔ ∀ (s : set α) (hs : is_compact s), @summable _ _ _ (uniform_on β s) F :=

(This is what Oliver and I were discussing in the other stream. See branch#compact-open-gluing for a sketch, with some sorries.)

Then you can use docs#summable_of_norm_bounded as I was suggesting, and your proof obligation becomes: prove that for any compact subset s of ℍ, there exists a summable nonnegative function M : ℤ × ℤ → ℝ, such that the sup-norm of Eise k x over the set s is at most M x. (You can do this using the "strip" argument which you have written the beginnings of.)

Let me know if you think this approach will work. I think it should be more efficient, in the sense of making the "end-user" (modular forms) files as short as possible.

[Chris Birkbeck]

Yes I think working with C(ℍ, ℂ) is a good idea, thank you. I'm busy today, but I'll start translating things into this language tomorrow and see how it goes.

[Chris Birkbeck]

Heather Macbeth said:

Chris Birkbeck Here's how I would set up the Eisenstein series construction. Following mathlib standard notation, denote by C(ℍ, ℂ) the space of continuous functions on the upper half-plane, equipped with the compact-open topology (i.e., the topology of locally uniform convergence). For now you would just like to construct $G_{2k}$ as an element of C(ℍ, ℂ), although eventually (when more complex analysis is available in mathlib) you will want to prove it is holomorphic.

Let's slightly modify what you wrote in your file and start by defining

def Eise (k : ℤ) (x : ℤ × ℤ) : C(ℍ, ℂ) :=
⟨λ z, 1/(x.1*z+x.2)^k, ... proof of continuity ...⟩

You want to prove ∀ k, summable (Eise k), i.e. that for each k the Eisenstein series is summable locally uniformly.

It will turn out that there is a family of seminorms on C(ℍ, ℂ), parametrized by the compact subsets s of ℍ, which induce topologies uniform_on ℂ s on C(ℍ, ℂ) (the topologies of uniform convergence on the s), with the following property:

lemma summable_compact_open_iff_forall [locally_compact_space α] [t2_space β] {ι : Type*}
  [decidable_eq ι] [nonempty ι] {l : filter ι} (F : ι → C(α, β)) :
  summable F
  ↔ ∀ (s : set α) (hs : is_compact s), @summable _ _ _ (uniform_on β s) F :=

(This is what Oliver and I were discussing in the other stream. See branch#compact-open-gluing for a sketch, with some sorries.)

Then you can use docs#summable_of_norm_bounded as I was suggesting, and your proof obligation becomes: prove that for any compact subset s of ℍ, there exists a summable nonnegative function M : ℤ × ℤ → ℝ, such that the sup-norm of Eise k x over the set s is at most M x. (You can do this using the "strip" argument which you have written the beginnings of.)

Let me know if you think this approach will work. I think it should be more efficient, in the sense of making the "end-user" (modular forms) files as short as possible.

@Heather Macbeth So I was just looking at some of the new additions relating to the compact-open topology. Has summable_compact_open_iff_forall also been PR'd? I couldn't find it.

[Heather Macbeth]

@Chris Birkbeck Sorry for not updating you. Since #9240 you can do

import topology.continuous_function.algebra
import topology.compact_open
import topology.algebra.infinite_sum

open_locale big_operators

variables {α : Type*} [topological_space α]
variables {β : Type*} [topological_space β] [add_comm_monoid β] [has_continuous_add β]

@[simp] lemma restrict_sum {ι : Type*} (I : finset ι) (F : ι → C(α, β)) (s : set α) :
  (∑ i in I, F i).restrict s = ∑ i in I, (F i).restrict s :=
by { ext x, simp }

lemma summable_compact_open_iff_forall [t2_space α] [locally_compact_space α] [t2_space β]
  {ι : Type*} [decidable_eq ι] [nonempty ι] {l : filter ι} (F : ι → C(α, β)) :
  summable F
  ↔ ∀ (s : set α) (hs : is_compact s), summable (λ i, (F i).restrict s) :=
by simpa using continuous_map.exists_tendsto_compact_open_iff_forall (λ I : finset ι, ∑ i in I, F i)

(in fact these should both be added as lemmas at some point). What's left (@Oliver Nash is working on it) is to show that on a compact space α, the compact-open topology is the same as the topology induced by the sup-norm.

[Oliver Nash]

It's true that I promised Heather I'm working on it but I must confess it will be at least a week before I take this up again, and furthermore this has been the case for several weeks!

[Oliver Nash]

(I do want to get to this though.)

[Chris Birkbeck]

Oh no don't worry, I was just wondering if I'd missed it! I'm not in a huge rush as the other complex analysis parts are still being done. But I'm glad this is still moving forward :)

[Chris Birkbeck]

Ok so #8979 now has a definition of modular forms , Eisenstein series and a sorry-free proof Eisenstein series are modular forms. Its still really just a "test area", i.e. a huge mess, but at least I can see now what things are good and bad with my current definition of modular forms. The main missing result was the "uniform limit of holomorphic functions is holomorphic" but it is possible to get this using #10000 (but what is in #8979 is probably not really the neatest way of doing this).

What I want to start thinking about is breaking this up into PR-able chunks. One of the first things that I want to fix with the current definition of modular forms are "coe" issues. For example, I defined the action of GL_pos (fin 2) ℝ on the upper_half_plane but at some points one wants to take a matrix in SL(2,ℤ) or some subgroup of this, and make them act on the upper_half_plane. But this ends up being a pain with how I've currently done it (at the moment there are lots of ugly coe lemmas to just get it done). Is there a particularly nice way to give an action of a group G on a set X which behaves nicely when restricting to subgroups of G or subgroups of subgroups of G and so on?

Similarly, I wonder if modular forms should be defined as functions ℂ → ℂ which satisfy some properties on ℍ. Instead of functions ℍ → ℂ. I think the former probably is probably a better fit with other things (such as differentiable_on), but also one sometimes wants to say things like f(1+z)=f(z) for z : ℍ, but one then needs to give ℍ an add_action ℤ ℍ, which one would have already if one worked with ℂ instead. That said, it does still make me uneasy having modular forms defined on all the complex numbers...

In any case, any ideas on how to approach there issues are most welcome!

[Kevin Buzzard]

I doubt SL_2(Z) is a subgroup of GL_pos(fin2) R as far as Lean is concerned!

[Chris Birkbeck]

Kevin Buzzard said:

I doubt SL_2(Z) is a subgroup of GL_pos(fin2) R as far as Lean is concerned!

OK you got me there! I guess I mean subgroups of SL(2,Z) coerced into GL_pos

[Kevin Buzzard]

If you define modular forms as functions on the complexes then you'd better have some extra axiom such as Im(z)<=0 -> f(z)=0, or else you'll run into problems with different functions agreeing on the upper half plane but not being equal modular forms. I don't see what's wrong with this approach though -- we use it in lots of other places. However GL_pos (fin 2) R and SL(2,Z) don't act on the complex numbers so then you get problems elsewhere.

[Kevin Buzzard]

Chris Birkbeck said:

Kevin Buzzard said:

I doubt SL_2(Z) is a subgroup of GL_pos(fin2) R as far as Lean is concerned!

OK you got me there! I guess I mean subgroups of SL(2,Z) coerced into GL_pos

We should surely have that if G -> H is a group hom and H acts on X then there's an induced action of G on X?

[Chris Birkbeck]

Kevin Buzzard said:

Chris Birkbeck said:

Kevin Buzzard said:

I doubt SL_2(Z) is a subgroup of GL_pos(fin2) R as far as Lean is concerned!

OK you got me there! I guess I mean subgroups of SL(2,Z) coerced into GL_pos

We should surely have that if G -> H is a group hom and H acts on X then there's an induced action of G on X?

ah yes good point. The issue might be that I didnt define them a group homs! just coes, I'll go back and check

[Johan Commelin]

Can scalar towers be used, so that you don't have to coerce so much?

[Chris Birkbeck]

Johan Commelin said:

Can scalar towers be used, so that you don't have to coerce so much?

Maybe. I must admit I've yet to look at how they work and how much they help with coe issues!

[Sebastien Gouezel]

Can you define modular forms as functions from $\mathbb{H}$ to $\mathbb{C}$ with the right equivariance property, and which are complex-differentiable (when you see $\mathbb{H}$ as a complex manifold)?

[Yaël Dillies]

Long story short, instead of coercing you can make groups act on each other, like A on B, C, D, B on C, D, C on D... Then is_scalar_towerwill state that the scalar multiplications associate with each other.

[Sebastien Gouezel]

(Unless you want to define them as sections of some vector bundle, for which the differential geometry machinery will be even more useful).

[Chris Birkbeck]

Sebastien Gouezel said:

Can you define modular forms as functions from $\mathbb{H}$ to $\mathbb{C}$ with the right equivariance property, and which are complex-differentiable (when you see $\mathbb{H}$ as a complex manifold)?

Yes this is something I was weighing up. When I first started I didn't know about mdifferentiable which would be one way of doing this. This is probably the most pleasing definition, but I don't know how well it would end up playing with the other analysis things

[Kevin Buzzard]

By which you mean you don't know how easy it would be to prove $\sum_{m,n}(mz+n)^{-k}$ is a modular form with this definition?

[Chris Birkbeck]

Yaël Dillies said:

Long story short, instead of coercing you can make groups act on each other, like A on B, C, D, B on C, D, C on D... Then is_scalar_towerwill state that the scalar multiplications associate with each other.

Aha I see, so I make all my groups act on each other via multiplication, but then also , each on the upper half plane? and then scalar_tower will say that the actions all work out?

[Chris Birkbeck]

Kevin Buzzard said:

By which you mean you don't know how easy it would be to prove $\sum_{m,n}(mz+n)^{-k}$ is a modular form with this definition?

Exactly!

[Kevin Buzzard]

But do you ever use this coercion from SL_2(Z) to SL_2(R) anyway? You'd be replacing it with an explicit function if you did this. Can you just make do with defining an action of SL_2(Z) on H?

[Chris Birkbeck]

It might be just as easy, I just haven't looked at mdifferentiable enough

[Chris Birkbeck]

Kevin Buzzard said:

But do you ever use this coercion from SL_2(Z) to SL_2(R) anyway? You'd be replacing it with an explicit function if you did this. Can you just make do with defining an action of SL_2(Z) on H?

Well eventually we'll want Hecke operators, so I wanted to use GL_pos for this reason.

[Kevin Buzzard]

But then you only need GL_2^+(Q)

[Chris Birkbeck]

Oh yeah, sure the reals are just there because I thought being more general would appease the mathlib gods more.

[Heather Macbeth]

Sebastien Gouezel said:

Can you define modular forms as functions from $\mathbb{H}$ to $\mathbb{C}$ with the right equivariance property, and which are complex-differentiable (when you see $\mathbb{H}$ as a complex manifold)?

I agree with this.

[Heather Macbeth]

And I still think that the Weierstrass M-test should be deduced as a simple consequence of the identification of the sup-norm topology with the compact-open topology -- did you encounter difficulties in doing it this way?

[Heather Macbeth]

@Chris Birkbeck See #11229; this should be able to replace your Weierstrass M-test.

[Chris Birkbeck]

Heather Macbeth said:

And I still think that the Weierstrass M-test should be deduced as a simple consequence of the identification of the sup-norm topology with the compact-open topology -- did you encounter difficulties in doing it this way?

Oh no I've just not gotten around to doing this way yet. Since I was just aiming for a sorry-free statement I just left the old version which I already had. My intention is to do it the way you suggested for the PR'ed version. Similarly, I think it was you who told me about mdifferentiable. I think this might be the way to go in the end, I just went with differentiable_on as a first attempt as that was what is in #10000

[Chris Birkbeck]

Heather Macbeth said:

Chris Birkbeck See #11229; this should be able to replace your Weierstrass M-test.

This looks great! exactly what is needed, thank you!