Argument principle

Stream: maths

[Muhammad Manji]

Hi all,

I'm trying to think about how to show on lean that the space of modular forms of level 1 (and later general levels) is finite dimensional using the valence formula i.e. avoiding more complicated geometric tools - I was wondering if there are good definitions of Laurent series and residues, or any version of the residue formula/argument principle for simple contours (e.g. circles, rectangles, things built up from these) on mathlib? If not, are there any serious obstacles to working on this?

[Johan Commelin]

We have Cauchy's integral theorem, but I don't think we have the residue formula yet. Is that right @Yury G. Kudryashov ?

[Yury G. Kudryashov]

You're right.

[Yury G. Kudryashov]

The main question is how to formulate these theorems.

[Riccardo Brasca]

If you want to start working on modular forms it's probably a good idea to coordinates the efforts. CC @Chris Birkbeck @Alex Kontorovich

[Yury G. Kudryashov]

I mean, in order to formulate the residue formula we need to be able to talk about points inside/outside of the contour.

[Johan Commelin]

But for certain contours this is easy, right? E.g. circles and rectangles.

[Yury G. Kudryashov]

Do you want to formulate each theorem many times?

[Muhammad Manji]

For this specific result the contour is a rectangle with some circles removed from it - so I'm hoping all that would be needed is a version for circles and one for rectangles

[Chris Birkbeck]

Riccardo Brasca said:

If you want to start working on modular forms it's probably a good idea to coordinates the efforts. CC Chris Birkbeck Alex Kontorovich

Yes I've already been talking to Muhhammad about this. In order to prove finite dimensionality for spaces of modular forms (even for levels different from 1) we just need to compute this one contour integral. But before that I guess we need some basics about residues and meromorphic functions.

[Chris Birkbeck]

I just don't know how hard it would be for these regions.

[Yury G. Kudryashov]

What is the integral? Does the function have poles of order >1? If not, then you can subtract $\sum \frac{a_i}{z-z_i}$ and use the fact that the integral of a differentiable function is zero (we have this for a rectangle and for a circle).

[Chris Birkbeck]

So you can see the region on page 19 of this: https://mdave16.github.io/notes/Modular%20Forms%20-%20Marc%20Masdeu.pdf

[Yury G. Kudryashov]

I don't know how to do it with the current state of complex analysis in mathlib.

[Oliver Nash]

image.png

[Chris Birkbeck]

Have any of the other theorem provers done contour integrals around things that aren't circles or rectangles?

[Oliver Nash]

Is the issue that we cannot state the integral for a path that is not a
Yury G. Kudryashov said:

use the fact that the integral of a differentiable function is zero (we have this for a rectangle and for a circle).

Is the issue that we cannot make the statement that the integral vanishes for curves that are not a rectangle / circle or that we do not have a proof?

[Anatole Dedecker]

Yury G. Kudryashov said:

I mean, in order to formulate the residue formula we need to be able to talk about points inside/outside of the contour.

The winding number for points outside the contour is zero so it doesn't matter, right ?

[Jireh Loreaux]

I think part of the problem is: what's your definition of winding number in the first place?

[Kalle Kytölä]

$$W_\gamma(z) = \frac{1}{2\pi i} \oint_\gamma (w-z)^{-1} \mathrm{d} w$$

Not a bad definition of winding number, right? If one combines with homotopy invariance for $\oint_\gamma$ and the fact that homotopy equivalence classes of paths in $\mathbb{C} \setminus \{ z \}$ contain piecewise smooth representatives, so the integral really makes sense for somebody in each equivalence class, isn't that more or less ok? :wink: :trolley:

Honestly, of course, I haven't given serious thought to the appropriate Lean-definition of winding number. Almost certainly Yury has. But at least in my courses I've actually taken the above as the starting point of residue calculus. And perhaps something like that is what Anatole had in mind?

[Kalle Kytölä]

That for a fixed $\gamma$ the function $z \mapsto W_\gamma(z)$ is locally constant and integer valued is "obvious". It would of course be nice to show that for Jordan curves, $W_\gamma^{-1} \{ 0 \}$ and $W_\gamma^{-1} \{ \pm1 \}$ are the two connected components of $\mathbb{C} \setminus \gamma$... :grinning_face_with_smiling_eyes: But that is not needed for residue calculus.