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.

def UpperHalfPlane.atImInfty : Filter UpperHalfPlane

Filter for approaching i∞.

Equations

• UpperHalfPlane.atImInfty = Filter.comap UpperHalfPlane.im Filter.atTop

theorem UpperHalfPlane.atImInfty_basis : Filter.HasBasis UpperHalfPlane.atImInfty (fun (x : ℝ) => True) fun (i : ℝ) => UpperHalfPlane.im ⁻¹' Set.Ici i

theorem UpperHalfPlane.atImInfty_mem (S : Set UpperHalfPlane) : S ∈ UpperHalfPlane.atImInfty ↔ ∃ (A : ℝ), ∀ (z : UpperHalfPlane), A ≤ UpperHalfPlane.im z → z ∈ S

def UpperHalfPlane.IsBoundedAtImInfty {α : Type u_1} [Norm α] (f : UpperHalfPlane → α) : Prop

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

Equations

• UpperHalfPlane.IsBoundedAtImInfty f = Filter.BoundedAtFilter UpperHalfPlane.atImInfty f

def UpperHalfPlane.IsZeroAtImInfty {α : Type u_1} [Zero α] [TopologicalSpace α] (f : UpperHalfPlane → α) : Prop

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

Equations

• UpperHalfPlane.IsZeroAtImInfty f = Filter.ZeroAtFilter UpperHalfPlane.atImInfty f

theorem UpperHalfPlane.zero_form_isBoundedAtImInfty {α : Type u_1} [NormedField α] : UpperHalfPlane.IsBoundedAtImInfty 0

def UpperHalfPlane.zeroAtImInftySubmodule (α : Type u_1) [NormedField α] : Submodule α (UpperHalfPlane → α)

Module of functions that are zero at infinity.

Equations

• UpperHalfPlane.zeroAtImInftySubmodule α = Filter.zeroAtFilterSubmodule UpperHalfPlane.atImInfty

def UpperHalfPlane.boundedAtImInftySubalgebra (α : Type u_1) [NormedField α] : Subalgebra α (UpperHalfPlane → α)

Subalgebra of functions that are bounded at infinity.

Equations

• UpperHalfPlane.boundedAtImInftySubalgebra α = Filter.boundedFilterSubalgebra UpperHalfPlane.atImInfty

theorem UpperHalfPlane.IsBoundedAtImInfty.mul {f : UpperHalfPlane → ℂ} {g : UpperHalfPlane → ℂ} (hf : UpperHalfPlane.IsBoundedAtImInfty f) (hg : UpperHalfPlane.IsBoundedAtImInfty g) : UpperHalfPlane.IsBoundedAtImInfty (f * g)

theorem UpperHalfPlane.bounded_mem (f : UpperHalfPlane → ℂ) : UpperHalfPlane.IsBoundedAtImInfty f ↔ ∃ (M : ℝ) (A : ℝ), ∀ (z : UpperHalfPlane), A ≤ UpperHalfPlane.im z → Complex.abs (f z) ≤ M

theorem UpperHalfPlane.zero_at_im_infty (f : UpperHalfPlane → ℂ) : UpperHalfPlane.IsZeroAtImInfty f ↔ ∀ (ε : ℝ), 0 < ε → ∃ (A : ℝ), ∀ (z : UpperHalfPlane), A ≤ UpperHalfPlane.im z → Complex.abs (f z) ≤ ε