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
- l.zero_at_filter f = filter.tendsto f l (nhds 0)
theorem
filter.zero_zero_at_filter
{α : Type u_1}
{β : Type u_2}
[has_zero β]
[topological_space β]
(l : filter α) :
l.zero_at_filter 0
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)
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)
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)
def
filter.zero_at_filter_submodule
{α : Type u_1}
{β : Type u_2}
[topological_space β]
[semiring β]
[has_continuous_add β]
[has_continuous_mul β]
(l : filter α) :
zero_at_filter_submodule l
is the submodule of f : α → β
which
tend to zero along l
.
Equations
- l.zero_at_filter_submodule = {carrier := l.zero_at_filter, add_mem' := _, zero_mem' := _, smul_mem' := _}
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
- l.zero_at_filter_add_submonoid = {carrier := l.zero_at_filter, add_mem' := _, zero_mem' := _}
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 : β) :
l.bounded_at_filter (function.const α 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) :
l.bounded_at_filter (f + 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) :
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) :
l.bounded_at_filter (c • 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) :
l.bounded_at_filter (f * g)
The submodule of functions that are bounded along a filter l
.
Equations
- l.bounded_filter_submodule = {carrier := l.bounded_at_filter, add_mem' := _, zero_mem' := _, smul_mem' := _}
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
.