mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(analysis/complex/upper_half_plane): Functions bounded at infinity

Open CBirkbeck opened this issue 3 years ago • 4 comments

The defines the notion of functions on the upper half plane being bounded at infinity and zero at infinity. This is required for #13250.

Open in Gitpod

CBirkbeck avatar Jun 27 '22 17:06 CBirkbeck

Please add a filter.has_basis statement about your filter (comes from at_top_basis.comap _).

urkud avatar Jun 28 '22 13:06 urkud

I'm on vacation for a few days. You may need to ping another maintainer if you want to have it reviewed earlier than July 6.

urkud avatar Jul 02 '22 12:07 urkud

Some cosmetic comments.

Thanks!

CBirkbeck avatar Jul 18 '22 21:07 CBirkbeck

Is there anything left to do here?

CBirkbeck avatar Jul 25 '22 08:07 CBirkbeck

Thanks!

bors d+

riccardobrasca avatar Sep 06 '22 15:09 riccardobrasca

:v: CBirkbeck can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors[bot] avatar Sep 06 '22 15:09 bors[bot]

bors r+

CBirkbeck avatar Sep 07 '22 14:09 CBirkbeck

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Sep 07 '22 17:09 bors[bot]