mathlib3 documentation

order.filter.zero_and_bounded_at_filter

Zero and Bounded at filter #

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

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_zero_at_filter {α : Type u_1} {β : Type u_2} [has_zero β] [topological_space β] (l : filter α) :
theorem filter.zero_at_filter.add {α : Type u_1} {β : Type u_2} [topological_space β] [add_zero_class β] [has_continuous_add β] {l : filter α} {f g : α β} (hf : l.zero_at_filter f) (hg : l.zero_at_filter g) :
theorem filter.zero_at_filter.neg {α : Type u_1} {β : Type u_2} [topological_space β] [add_group β] [has_continuous_neg β] {l : filter α} {f : α β} (hf : l.zero_at_filter f) :
theorem filter.zero_at_filter.smul {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} [topological_space 𝕜] [topological_space β] [has_zero 𝕜] [has_zero β] [smul_with_zero 𝕜 β] [has_continuous_smul 𝕜 β] {l : filter α} {f : α β} (c : 𝕜) (hf : l.zero_at_filter f) :
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 β] (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_add_comm_group β] {l : filter α} {f : α β} (hf : l.zero_at_filter f) :
theorem filter.const_bounded_at_filter {α : Type u_1} {β : Type u_2} [normed_field β] (l : filter α) (c : β) :
theorem filter.bounded_at_filter.add {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {l : filter α} {f g : α β} (hf : l.bounded_at_filter f) (hg : l.bounded_at_filter g) :
theorem filter.bounded_at_filter.neg {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {l : filter α} {f : α β} (hf : l.bounded_at_filter f) :
theorem filter.bounded_at_filter.smul {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} [normed_field 𝕜] [normed_add_comm_group β] [normed_space 𝕜 β] {l : filter α} {f : α β} (c : 𝕜) (hf : l.bounded_at_filter f) :
theorem filter.bounded_at_filter.mul {α : Type u_1} {β : Type u_2} [normed_field β] {l : filter α} {f g : α β} (hf : l.bounded_at_filter f) (hg : l.bounded_at_filter g) :
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