Documentation

Mathlib.Order.Filter.ZeroAndBoundedAtFilter

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.

source
def Filter.ZeroAtFilter {α : Type u_2} {β : Type u_3} [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
Instances For
    source
    theorem Filter.zero_zeroAtFilter {α : Type u_2} {β : Type u_3} [Zero β] [TopologicalSpace β] (l : Filter α) :
    l.ZeroAtFilter 0
    source
    theorem Filter.ZeroAtFilter.add {α : Type u_2} {β : Type u_3} [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] {l : Filter α} {f g : α → β} (hf : l.ZeroAtFilter f) (hg : l.ZeroAtFilter g) :
    l.ZeroAtFilter (f + g)
    source
    theorem Filter.ZeroAtFilter.neg {α : Type u_2} {β : Type u_3} [TopologicalSpace β] [AddGroup β] [ContinuousNeg β] {l : Filter α} {f : α → β} (hf : l.ZeroAtFilter f) :
    l.ZeroAtFilter (-f)
    source
    theorem Filter.ZeroAtFilter.smul {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] [Zero 𝕜] [Zero β] [SMulWithZero 𝕜 β] [ContinuousConstSMul 𝕜 β] {l : Filter α} {f : α → β} (c : 𝕜) (hf : l.ZeroAtFilter f) :
    l.ZeroAtFilter (c • f)
    source
    def Filter.zeroAtFilterSubmodule (𝕜 : Type u_1) {α : Type u_2} {β : Type u_3} [TopologicalSpace β] [Semiring 𝕜] [AddCommMonoid β] [Module 𝕜 β] [ContinuousAdd β] [ContinuousConstSMul 𝕜 β] (l : Filter α) :
    Submodule 𝕜 (α → β)

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

    Equations
    Instances For
      source
      def Filter.zeroAtFilterAddSubmonoid {α : Type u_2} {β : Type u_3} [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] (l : Filter α) :
      AddSubmonoid (α → β)

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

      Equations
      • l.zeroAtFilterAddSubmonoid = { carrier := l.ZeroAtFilter, add_mem' := ⋯, zero_mem' := ⋯ }
      Instances For
        source
        def Filter.BoundedAtFilter {α : Type u_2} {β : Type u_3} [Norm β] (l : Filter α) (f : α → β) :
        Prop

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

        Equations
        • l.BoundedAtFilter f = f =O[l] 1
        Instances For
          source
          theorem Filter.ZeroAtFilter.boundedAtFilter {α : Type u_2} {β : Type u_3} [SeminormedAddGroup β] {l : Filter α} {f : α → β} (hf : l.ZeroAtFilter f) :
          l.BoundedAtFilter f
          source
          theorem Filter.const_boundedAtFilter {α : Type u_2} {β : Type u_3} [Norm β] (l : Filter α) (c : β) :
          l.BoundedAtFilter (Function.const α c)
          source
          theorem Filter.BoundedAtFilter.add {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup β] {l : Filter α} {f g : α → β} (hf : l.BoundedAtFilter f) (hg : l.BoundedAtFilter g) :
          l.BoundedAtFilter (f + g)
          source
          theorem Filter.BoundedAtFilter.neg {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup β] {l : Filter α} {f : α → β} (hf : l.BoundedAtFilter f) :
          l.BoundedAtFilter (-f)
          source
          theorem Filter.BoundedAtFilter.smul {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [SeminormedRing 𝕜] [SeminormedAddCommGroup β] [Module 𝕜 β] [BoundedSMul 𝕜 β] {l : Filter α} {f : α → β} (c : 𝕜) (hf : l.BoundedAtFilter f) :
          l.BoundedAtFilter (c • f)
          source
          theorem Filter.BoundedAtFilter.mul {α : Type u_2} {β : Type u_3} [SeminormedRing β] {l : Filter α} {f g : α → β} (hf : l.BoundedAtFilter f) (hg : l.BoundedAtFilter g) :
          l.BoundedAtFilter (f * g)
          source
          def Filter.boundedFilterSubmodule (𝕜 : Type u_1) {α : Type u_2} {β : Type u_3} [SeminormedRing 𝕜] [SeminormedAddCommGroup β] [Module 𝕜 β] [BoundedSMul 𝕜 β] (l : Filter α) :
          Submodule 𝕜 (α → β)

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

          Equations
          Instances For
            source
            def Filter.boundedFilterSubalgebra (𝕜 : Type u_1) {α : Type u_2} {β : Type u_3} [SeminormedCommRing 𝕜] [SeminormedRing β] [Algebra 𝕜 β] [BoundedSMul 𝕜 β] (l : Filter α) :
            Subalgebra 𝕜 (α → β)

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

            Equations
            Instances For