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.

source
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
source
theorem filter.zero_zero_at_filter {α : Type u_1} {β : Type u_2} [has_zero β] [topological_space β] (l : filter α) :
l.zero_at_filter 0
source
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) :
l.zero_at_filter (f + g)
source
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) :
l.zero_at_filter (-f)
source
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) :
l.zero_at_filter (c • f)
source
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
source
def filter.zero_at_filter_add_submonoid {α : Type u_1} {β : Type u_2} [topological_space β] [add_zero_class β] [has_continuous_add β] (l : filter α) :
add_submonoid (α → β)

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

Equations
source
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
source
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) :
l.bounded_at_filter f
source
theorem filter.const_bounded_at_filter {α : Type u_1} {β : Type u_2} [normed_field β] (l : filter α) (c : β) :
l.bounded_at_filter (function.const α c)
source
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) :
l.bounded_at_filter (f + g)
source
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) :
l.bounded_at_filter (-f)
source
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) :
l.bounded_at_filter (c • f)
source
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) :
l.bounded_at_filter (f * g)
source
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
source
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