Functions bounded at infinity #15009

Stream: PR reviews

[Chris Birkbeck]

Does anyone have a moment to look at #15009 ? I'd like to get the modular form definition PR'd but this is holding things back.

[Moritz Doll]

I will look at this later more carefully, but I think the docstrings are a bit weird (and maybe the naming as well). For me $i \infty$ would be the point at infinity after radially compactifying $\mathbb{C}$ and then restricting to the closure of $\mathbb{H}$. So a function that is constant in the imaginary part part would be bounded at $i \infty$ for me, but it is not for your definition.
Maybe the renaming it the definition to at_im_infty would be better?

Also if your definition is at_foo, then all the lemmas should be baz_at_foo so even if you insist on at_I_infty, then the lemmas should be baz_at_I_infty, not baz_at_infty.

[Moritz Doll]

even if you do the 1-point compactification and then restrict to $\mathbb{H}$ your condition is weird. For modular forms it is the correct one, but that relies on the fact that modular forms are periodic in the real part.

[Moritz Doll]

don't you just want bounded at infinity (where infinity is the usual infinity + the real axis) and because modular surface has exactly one cusp this is the same as your condition?

[Chris Birkbeck]

Sure I'm happy to change the name to at_im_infty. I was only thinking about the upper half space and mod forms so this is why I went with this definition of infinity. If its preferable I could change to other infinity (with the real axis) but I'd have to think about how to do this...

[Moritz Doll]

I think you certainly want to have this definition as it is very convenient to work with and I don't think you should change anything major in this PR. I am just nitpicking the name and the docstrings.

Another possibility is to say that you are bounding in horocycles that touches the boundary at $i \infty$. In that picture the reference to $i \infty$ is again valid, but I did not see any mentions to horocycles. But I think this is a better approach when defining things in the disk model and then we would have lemma that says that at_im_infty in the upper-half plane is equivalent to at_horocycle i (or whatever point gets mapped to infinity) in disk model.

[Antoine Chambert-Loir]

Chris Birkbeck said:

Does anyone have a moment to look at #15009 ? I'd like to get the modular form definition PR'd but this is holding things back.

Remark on names: why is_bound_at_infty (line 48) and not is_bounded_at_infty like you say in the docstring?

[Chris Birkbeck]

:ping_pong:

[Chris Birkbeck]

Antoine Chambert-Loir said:

Chris Birkbeck said:

Does anyone have a moment to look at #15009 ? I'd like to get the modular form definition PR'd but this is holding things back.

Remark on names: why is_bound_at_infty (line 48) and not is_bounded_at_infty like you say in the docstring?

that was just a typo