# Bounded at infinity #

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

Filter for approaching i∞.

Equations
Instances For
theorem UpperHalfPlane.atImInfty_basis :
UpperHalfPlane.atImInfty.HasBasis (fun (x : ) => True) fun (i : ) =>
theorem UpperHalfPlane.atImInfty_mem (S : ) :
∃ (A : ), ∀ (z : UpperHalfPlane), A z.imz S
def UpperHalfPlane.IsBoundedAtImInfty {α : Type u_1} [Norm α] (f : ) :

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

Equations
Instances For
def UpperHalfPlane.IsZeroAtImInfty {α : Type u_1} [Zero α] [] (f : ) :

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

Equations
Instances For

Module of functions that are zero at infinity.

Equations
Instances For

Subalgebra of functions that are bounded at infinity.

Equations
Instances For
theorem UpperHalfPlane.bounded_mem (f : ) :
∃ (M : ) (A : ), ∀ (z : UpperHalfPlane), A z.imComplex.abs (f z) M
theorem UpperHalfPlane.zero_at_im_infty (f : ) :
∀ (ε : ), 0 < ε∃ (A : ), ∀ (z : UpperHalfPlane), A z.imComplex.abs (f z) ε