Products of Modular Forms

Stream: Is there code for X?

[Archie Browne]

Are the following facts in Mathlib or elsewhere? Assume
(n : ℕ) (k : ℤ) (Γ : Subgroup (GL (Fin 2) ℝ)) (γ : Fin n → ModularForm Γ k).

1. The product fun z ↦ ∏ i : Fin n, (γ i) z is a modular form. The case of just two functions is
   ModularForm.mul.

2. If ∀ z, ∏ i : Fin n, (γ i) z = 0, then ∃ i, ∀ z, (γ i) z = 0. There is a version on two Analytic functions
   (AnalyticOnNhd.eq_zero_or_eq_zero_of_mul_eq_zero or AnalyticOn.eq_zero_or_eq_zero_of_mul_eq_zero)
   and I can prove the modular form version with two functions from either of these. Extending this to n Modular Forms by induction wouldn't be too trcky but it would be nice if it was already there. It would also be useful to have point 1. for this.

If these aren't there, any tips on design that would be preferable would also be appreciated. Thanks.

[Michael Stoll]

@David Loeffler @Chris Birkbeck

[Chris Birkbeck]

So we don't have 1), but that should be easy using ModularForm.mul. I have a version of 2 in a repo and I was planning on using this now that we have the norm on modular forms to finish off the proof that for finite index subgroups the spaces of modular forms are finite dimentional (using that we have this for level 1). But PRing both of these 1 would be welcome!

[Chris Birkbeck]

Edit: Ignore this, see below.

[Chris Birkbeck]

You can find this stuff here: https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean/tree/ModForm_GenFinDim

[Chris Birkbeck]

Oh actually, 2 was basically done in the norm PR. See docs#UpperHalfPlane.prod_eq_zero_iff

[Archie Browne]

Ah great thank you! I was also interested in these for the finite dimensional result haha. So if I understand, 1) is still not done? I'll take a look.

[Chris Birkbeck]

Yeah so, I don't think we have 1, that would be something good to PR to mathlib. For the fin dim result, you can see in the branch of the sphere packing repo above what I had started experimenting with. Now that we have the norm, I think we are close now.

[David Loeffler]

I agree that the general finite-dimensionality is not far off now, but there is a certain amount of work still to be done. The compactness results in my PR #30089 (currently being reviewed by Chris B) are one step towards this.

My next step was going to be to show that if f is a modular form of level Γ (and any weight), then the order of vanishing of f at z depends only on the Γ-orbit of z. This is fiddly; I have the code ready but it needs a little cleanup. Using that & norm maps & compactness of truncated fundamental domain one deduces that there are only finitely many Γ-orbits where the order of vanishing is positive.

With this in hand, one can argue that if g \in M_k(Γ) vanishes to high enough order at some finite set of points, then it must be a multiple of f by something in M_0(Γ) (which we know is 1-dimensional). This exhibits a linear map from M_k(Γ) to a finite-dimensional space whose kernel is finite-dimensional, hence M_k(Γ) is also finite-dimensional.

Happy to coordinate on this with anyone who's interested.

[Archie Browne]

Okay thanks - I've made a PR at #32978