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

instance UpperHalfPlane.instNeBotAtImInfty : atImInfty.NeBot

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

theorem UpperHalfPlane.atImInfty_mem (S : Set UpperHalfPlane) : S ∈ 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.

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

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

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

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

Module of functions that are zero at infinity.

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

Subalgebra of functions that are bounded at infinity.

theorem UpperHalfPlane.isBoundedAtImInfty_iff {α : Type u_1} [Norm α] {f : UpperHalfPlane → α} : IsBoundedAtImInfty f ↔ ∃ (M : ℝ) (A : ℝ), ∀ (z : UpperHalfPlane), A ≤ z.im → ‖f z‖ ≤ M

theorem UpperHalfPlane.isZeroAtImInfty_iff {α : Type u_1} [SeminormedAddGroup α] {f : UpperHalfPlane → α} : IsZeroAtImInfty f ↔ ∀ (ε : ℝ), 0 < ε → ∃ (A : ℝ), ∀ (z : UpperHalfPlane), A ≤ z.im → ‖f z‖ ≤ ε

theorem UpperHalfPlane.IsZeroAtImInfty.isBoundedAtImInfty {α : Type u_1} [SeminormedAddGroup α] {f : UpperHalfPlane → α} (hf : IsZeroAtImInfty f) : IsBoundedAtImInfty f

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

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

theorem UpperHalfPlane.tendsto_smul_atImInfty {g : GL (Fin 2) ℝ} (hg : ↑g 1 0 = 0) : Filter.Tendsto (fun (τ : UpperHalfPlane) => g • τ) atImInfty atImInfty