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 : UpperHalfPlane.atImInfty.HasBasis (fun (x : ℝ) => True) fun (i : ℝ) => UpperHalfPlane.im ⁻¹' Set.Ici i

theorem UpperHalfPlane.atImInfty_mem (S : Set UpperHalfPlane) : S ∈ UpperHalfPlane.atImInfty ↔ ∃ (A : ℝ), ∀ (z : UpperHalfPlane), A ≤ z.im → 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 = UpperHalfPlane.atImInfty.BoundedAtFilter 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 = UpperHalfPlane.atImInfty.ZeroAtFilter 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 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 ≤ z.im → Complex.abs (f z) ≤ M

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

theorem UpperHalfPlane.tendsto_comap_im_ofComplex : Filter.Tendsto (↑UpperHalfPlane.ofComplex) (Filter.comap Complex.im Filter.atTop) UpperHalfPlane.atImInfty

theorem UpperHalfPlane.tendsto_coe_atImInfty : Filter.Tendsto UpperHalfPlane.coe UpperHalfPlane.atImInfty (Filter.comap Complex.im Filter.atTop)