Documentation

Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

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∞.

Instances For

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

    Instances For

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

      Instances For

        Module of functions that are zero at infinity.

        Instances For

          Subalgebra of functions that are bounded at infinity.

          Instances For