mathlib3 documentation


Bounded at infinity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For complex valued functions on the upper half plane, this file defines the filter at_im_infty required for defining when functions are bounded at infinity and zero at infinity. Both of which are relevant for defining modular forms.

A function f : ℍ → α is bounded at infinity if it is bounded along at_im_infty.


A function f : ℍ → α is zero at infinity it is zero along at_im_infty.