Zero and Bounded at filter

Given a filter l we define the notion of a function being ZeroAtFilter as well as being BoundedAtFilter. Alongside this we construct the Submodule, AddSubmonoid of functions that are ZeroAtFilter. Similarly, we construct the Submodule and Subalgebra of functions that are BoundedAtFilter.

def Filter.ZeroAtFilter {α : Type u_1} {β : Type u_2} [Zero β] [TopologicalSpace β] (l : Filter α) (f : α → β) : Prop

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

Equations

• Filter.ZeroAtFilter l f = Filter.Tendsto f l (nhds 0)

theorem Filter.zero_zeroAtFilter {α : Type u_1} {β : Type u_2} [Zero β] [TopologicalSpace β] (l : Filter α) : Filter.ZeroAtFilter l 0

theorem Filter.ZeroAtFilter.add {α : Type u_1} {β : Type u_2} [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] {l : Filter α} {f : α → β} {g : α → β} (hf : Filter.ZeroAtFilter l f) (hg : Filter.ZeroAtFilter l g) : Filter.ZeroAtFilter l (f + g)

theorem Filter.ZeroAtFilter.neg {α : Type u_1} {β : Type u_2} [TopologicalSpace β] [AddGroup β] [ContinuousNeg β] {l : Filter α} {f : α → β} (hf : Filter.ZeroAtFilter l f) : Filter.ZeroAtFilter l (-f)

theorem Filter.ZeroAtFilter.smul {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} [TopologicalSpace 𝕜] [TopologicalSpace β] [Zero 𝕜] [Zero β] [SMulWithZero 𝕜 β] [ContinuousSMul 𝕜 β] {l : Filter α} {f : α → β} (c : 𝕜) (hf : Filter.ZeroAtFilter l f) : Filter.ZeroAtFilter l (c • f)

def Filter.zeroAtFilterSubmodule {α : Type u_1} {β : Type u_2} [TopologicalSpace β] [Semiring β] [ContinuousAdd β] [ContinuousMul β] (l : Filter α) : Submodule β (α → β)

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

Equations

• One or more equations did not get rendered due to their size.

def Filter.zeroAtFilterAddSubmonoid {α : Type u_1} {β : Type u_2} [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] (l : Filter α) : AddSubmonoid (α → β)

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

Equations

• One or more equations did not get rendered due to their size.

def Filter.BoundedAtFilter {α : Type u_1} {β : Type u_2} [Norm β] (l : Filter α) (f : α → β) : Prop

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

Equations

• Filter.BoundedAtFilter l f = f =O[l] 1

theorem Filter.ZeroAtFilter.boundedAtFilter {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} {f : α → β} (hf : Filter.ZeroAtFilter l f) : Filter.BoundedAtFilter l f

theorem Filter.const_boundedAtFilter {α : Type u_1} {β : Type u_2} [NormedField β] (l : Filter α) (c : β) : Filter.BoundedAtFilter l (Function.const α c)

theorem Filter.BoundedAtFilter.add {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} {f : α → β} {g : α → β} (hf : Filter.BoundedAtFilter l f) (hg : Filter.BoundedAtFilter l g) : Filter.BoundedAtFilter l (f + g)

theorem Filter.BoundedAtFilter.neg {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} {f : α → β} (hf : Filter.BoundedAtFilter l f) : Filter.BoundedAtFilter l (-f)

theorem Filter.BoundedAtFilter.smul {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} [NormedField 𝕜] [NormedAddCommGroup β] [NormedSpace 𝕜 β] {l : Filter α} {f : α → β} (c : 𝕜) (hf : Filter.BoundedAtFilter l f) : Filter.BoundedAtFilter l (c • f)

theorem Filter.BoundedAtFilter.mul {α : Type u_1} {β : Type u_2} [NormedField β] {l : Filter α} {f : α → β} {g : α → β} (hf : Filter.BoundedAtFilter l f) (hg : Filter.BoundedAtFilter l g) : Filter.BoundedAtFilter l (f * g)

def Filter.boundedFilterSubmodule {α : Type u_1} {β : Type u_2} [NormedField β] (l : Filter α) : Submodule β (α → β)

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

Equations

• One or more equations did not get rendered due to their size.

def Filter.boundedFilterSubalgebra {α : Type u_1} {β : Type u_2} [NormedField β] (l : Filter α) : Subalgebra β (α → β)

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

Equations

• One or more equations did not get rendered due to their size.