Bounded at infinity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

def upper_half_plane.at_im_infty :

filter upper_half_plane

Filter for approaching i∞.

Equations

upper_half_plane.at_im_infty = filter.comap upper_half_plane.im filter.at_top

source

theorem upper_half_plane.at_im_infty_basis :

upper_half_plane.at_im_infty.has_basis (λ (_x : ℝ), true) (λ (i : ℝ), upper_half_plane.im ⁻¹' set.Ici i)

source

theorem upper_half_plane.at_im_infty_mem (S : set upper_half_plane) :

S ∈ upper_half_plane.at_im_infty ↔ ∃ (A : ℝ), ∀ (z : upper_half_plane), A ≤ z.im → z ∈ S

source

def upper_half_plane.is_bounded_at_im_infty {α : Type u_1} [has_norm α] (f : upper_half_plane → α) :

Prop

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

Equations

upper_half_plane.is_bounded_at_im_infty f = upper_half_plane.at_im_infty.bounded_at_filter f

source

def upper_half_plane.is_zero_at_im_infty {α : Type u_1} [has_zero α] [topological_space α] (f : upper_half_plane → α) :

Prop

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

Equations

upper_half_plane.is_zero_at_im_infty f = upper_half_plane.at_im_infty.zero_at_filter f

source

theorem upper_half_plane.zero_form_is_bounded_at_im_infty {α : Type u_1} [normed_field α] :

upper_half_plane.is_bounded_at_im_infty 0

source

def upper_half_plane.zero_at_im_infty_submodule (α : Type u_1) [normed_field α] :

submodule α (upper_half_plane → α)

Module of functions that are zero at infinity.

Equations

upper_half_plane.zero_at_im_infty_submodule α = upper_half_plane.at_im_infty.zero_at_filter_submodule

source

def upper_half_plane.bounded_at_im_infty_subalgebra (α : Type u_1) [normed_field α] :

subalgebra α (upper_half_plane → α)

ubalgebra of functions that are bounded at infinity.

Equations

upper_half_plane.bounded_at_im_infty_subalgebra α = upper_half_plane.at_im_infty.bounded_filter_subalgebra

source

theorem upper_half_plane.is_bounded_at_im_infty.mul {f g : upper_half_plane → ℂ} (hf : upper_half_plane.is_bounded_at_im_infty f) (hg : upper_half_plane.is_bounded_at_im_infty g) :

upper_half_plane.is_bounded_at_im_infty (f * g)

source

theorem upper_half_plane.bounded_mem (f : upper_half_plane → ℂ) :

upper_half_plane.is_bounded_at_im_infty f ↔ ∃ (M A : ℝ), ∀ (z : upper_half_plane), A ≤ z.im → ⇑complex.abs (f z) ≤ M

source

theorem upper_half_plane.zero_at_im_infty (f : upper_half_plane → ℂ) :

upper_half_plane.is_zero_at_im_infty f ↔ ∀ (ε : ℝ), 0 < ε → (∃ (A : ℝ), ∀ (z : upper_half_plane), A ≤ z.im → ⇑complex.abs (f z) ≤ ε)