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.