Theorems · Inductive type · functional analysis

Asymptotics.IsLittleOTVS

(𝕜 : Type u_1) →
  {α : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        [ENorm 𝕜] →
          [TopologicalSpace E] →
            [TopologicalSpace F] → [Zero E] → [Zero F] → [SMul 𝕜 E] → [SMul 𝕜 F] → Filter α → (α → E) → (α → F) → Prop

f =o[𝕜; l] g (IsLittleOTVS 𝕜 l f g) is a generalization of f =o[l] g (IsLittleO l f g) that works in topological 𝕜-vector spaces. Given two functions f and g taking values in topological vector spaces over a normed field K, we say that $f = o(g)$ if for any neighborhood of zero U in the codomain of f there exists a neighborhood of zero V in the codomain of g such that $\operatorname{gauge}_{K, U} (f(x)) = o(\operatorname{gauge}_{K, V} (g(x)))$, where $\operatorname{gauge}_{K, U}(y) = \inf \{‖c‖ \mid y ∈ c • U\}$. We use an ENNReal-valued function egauge for the gauge, so we unfold the definition of little o instead of reusing it.

Defined in

Mathlib.Analysis.Asymptotics.TVS

Cited by

73 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

ENormTopologicalSpaceTopologicalSpaceZeroZeroSMulSMul