mathlib documentation

order.filter.zero_and_bounded_at_filter

Zero and Bounded at filter #

Given a filter l we define the notion of a function being zero_at_filter as well as being bounded_at_filter. Alongside this we construct the submodule, add_submonoid of functions that are zero_at_filter. Similarly, we construct the submodule and subalgebra of functions that are bounded_at_filter.

def filter.zero_at_filter {α : Type u_1} {β : Type u_2} [has_zero β] [topological_space β] (l : filter α) (f : α β) :
Prop

If l is a filter on α, then a function f : α → β is zero_at_filter l if it tends to zero along l.

Equations
theorem filter.zero_is_zero_at_filter {α : Type u_1} {β : Type u_2} [has_zero β] [topological_space β] (l : filter α) :
def filter.zero_at_filter_submodule {α : Type u_1} {β : Type u_2} [topological_space β] [semiring β] [has_continuous_add β] [has_continuous_mul β] (l : filter α) :
submodule β β)

zero_at_filter_submodule l is the submodule of f : α → β which tend to zero along l.

Equations

zero_at_filter_add_submonoid l is the additive submonoid of f : α → β which tend to zero along l.

Equations
def filter.bounded_at_filter {α : Type u_1} {β : Type u_2} [has_norm β] [has_one β)] (l : filter α) (f : α β) :
Prop

If l is a filter on α, then a function f: α → β is bounded_at_filter l if f =O[l] 1.

Equations
theorem filter.zero_at_filter.bounded_at_filter {α : Type u_1} {β : Type u_2} [normed_field β] {l : filter α} {f : α β} (hf : l.zero_at_filter f) :
theorem filter.zero_is_bounded_at_filter {α : Type u_1} {β : Type u_2} [normed_field β] (l : filter α) :
def filter.bounded_filter_submodule {α : Type u_1} {β : Type u_2} [normed_field β] (l : filter α) :
submodule β β)

The submodule of functions that are bounded along a filter l.

Equations
def filter.bounded_filter_subalgebra {α : Type u_1} {β : Type u_2} [normed_field β] (l : filter α) :
subalgebra β β)

The subalgebra of functions that are bounded along a filter l.

Equations