Mathlib.Analysis.Asymptotics.TVS

Module docstring

{"# Asymptotics in a Topological Vector Space

This file defines Asymptotics.IsLittleOTVS as a generalization of Asymptotics.IsLittleO from normed spaces to topological 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\}$.

In a normed space, we can use balls of positive radius as both U and V, thus reducing the definition to the classical one.

This frees the user from having to chose a canonical norm, at the expense of having to pick a specific base ring. This is exactly the tradeoff we want in HasFDerivAtFilter, as there the base ring is already chosen, and this removes the choice of norm being part of the statement.

This definition was added to the library in order to migrate Fréchet derivatives from normed vector spaces to topological vector spaces. The definition is motivated by https://en.wikipedia.org/wiki/Fr%C3%A9chetderivative#Generalizationtotopologicalvector_spaces but the definition there doesn't work for topological vector spaces over general normed fields. This Zulip discussion led to the current choice of the definition.

It may be possible to generalize $f = O(g)$ and $f = \Theta(g)$ in a similar way, but we don't need these definitions to redefine Fréchet derivatives, so formalization of these generalizations is left for later, until someone will need it (e.g., to prove properties of the Fréchet derivative over TVS).

Main results

isLittleOTVS_iff_isLittleO: the equivalence between these two definitions in the case of a normed space.
isLittleOTVS_iff_tendsto_inv_smul: the equivalence to convergence of the ratio to zero in case of a topological vector space.

Asymptotics.IsLittleOTVS definition

 (𝕜 : Type*) {α E F : Type*} [NNNorm 𝕜] [TopologicalSpace E] [TopologicalSpace F] [Zero E] [Zero F] [SMul 𝕜 E]
  [SMul 𝕜 F] (l : Filter α) (f : α → E) (g : α → F) : Prop

Full source

/-- `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. -/
def IsLittleOTVS (𝕜 : Type*) {α E F : Type*}
    [NNNorm 𝕜] [TopologicalSpace E] [TopologicalSpace F] [Zero E] [Zero F] [SMul 𝕜 E] [SMul 𝕜 F]
    (l : Filter α) (f : α → E) (g : α → F) : Prop :=
  ∀ U ∈ 𝓝 (0 : E), ∃ V ∈ 𝓝 (0 : F), ∀ ε ≠ (0 : ℝ≥0),
    ∀ᶠ x in l, egauge 𝕜 U (f x) ≤ ε * egauge 𝕜 V (g x)

Little-o relation in topological vector spaces

Informal description

Given a normed field $\mathbb{K}$ with a non-negative norm, topological vector spaces $E$ and $F$ over $\mathbb{K}$ (each equipped with a topology and a zero element), and a filter $l$ on a type $\alpha$, we say that a function $f : \alpha \to E$ is asymptotically dominated by $g : \alpha \to F$ (denoted $f = o_{\mathbb{K}, l}(g)$) if for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $F$ such that for every positive real $\varepsilon > 0$, the inequality $\text{egauge}_{\mathbb{K}, U}(f(x)) \leq \varepsilon \cdot \text{egauge}_{\mathbb{K}, V}(g(x))$ holds for all $x$ in $l$ eventually. Here, $\text{egauge}_{\mathbb{K}, U}(y) = \inf \{ \|c\| \mid c \in \mathbb{K}, y \in c \cdot U \}$ is the Minkowski functional (gauge) of $U$ at $y$.

Asymptotics.term_=o[_;_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:100 f " =o[" 𝕜 "; " l "] " g:100 => IsLittleOTVS 𝕜 l f g

Little-o notation in topological vector spaces

Informal description

Given a normed field $\mathbb{K}$, topological vector spaces $E$ and $F$ over $\mathbb{K}$, and a filter $l$ on a type $\alpha$, we say that a function $f : \alpha \to E$ is little-o of $g : \alpha \to F$ (written $f = o_{\mathbb{K}, l}(g)$) if for every neighborhood of zero $U$ in $E$, there exists a neighborhood of zero $V$ in $F$ such that the gauge function $\operatorname{gauge}_{\mathbb{K}, U}(f(x))$ is little-o of $\operatorname{gauge}_{\mathbb{K}, V}(g(x))$ as $x$ tends to $l$. Here, $\operatorname{gauge}_{\mathbb{K}, U}(y) = \inf \{ \|c\| \mid y \in c \cdot U \}$. This definition generalizes the classical little-o notation from normed spaces to topological vector spaces by using gauge functions instead of norms.

Asymptotics.isLittleOTVS_congr theorem

(hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₁ =o[𝕜; l] g₁ ↔ f₂ =o[𝕜; l] g₂

Full source

theorem isLittleOTVS_congr (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
    f₁ =o[𝕜; l] g₁f₁ =o[𝕜; l] g₁ ↔ f₂ =o[𝕜; l] g₂ := by
  simp only [IsLittleOTVS]
  refine forall₂_congr fun U hU => exists_congr fun V => and_congr_right fun hV =>
    forall₂_congr fun ε hε => Filter.eventually_congr ?_
  filter_upwards [hf, hg] with _ e₁ e₂
  rw [e₁, e₂]

Asymptotic Dominance is Preserved Under Eventual Equality

Informal description

Let $\mathbb{K}$ be a normed field, $\alpha$ a type, and $E$, $F$ topological vector spaces over $\mathbb{K}$ with zero elements. Let $l$ be a filter on $\alpha$, and $f_1, f_2 : \alpha \to E$, $g_1, g_2 : \alpha \to F$ be functions. If $f_1$ and $f_2$ are eventually equal along $l$, and $g_1$ and $g_2$ are eventually equal along $l$, then $f_1$ is asymptotically dominated by $g_1$ (denoted $f_1 = o_{\mathbb{K}, l}(g_1)$) if and only if $f_2$ is asymptotically dominated by $g_2$ (denoted $f_2 = o_{\mathbb{K}, l}(g_2)$).

Asymptotics.IsLittleOTVS.congr' theorem

(h : f₁ =o[𝕜; l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₂ =o[𝕜; l] g₂

Full source

/-- A stronger version of `IsLittleOTVS.congr` that requires the functions only agree along the
filter. -/
theorem IsLittleOTVS.congr' (h : f₁ =o[𝕜; l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
    f₂ =o[𝕜; l] g₂ :=
  (isLittleOTVS_congr hf hg).mp h

Asymptotic Little-o Relation is Preserved Under Eventual Equality

Informal description

Let $\mathbb{K}$ be a normed field, $\alpha$ a type, and $E$, $F$ topological vector spaces over $\mathbb{K}$ with zero elements. Let $l$ be a filter on $\alpha$, and $f_1, f_2 : \alpha \to E$, $g_1, g_2 : \alpha \to F$ be functions. If $f_1 = o_{\mathbb{K}, l}(g_1)$, and $f_1$ and $f_2$ are eventually equal along $l$, and $g_1$ and $g_2$ are eventually equal along $l$, then $f_2 = o_{\mathbb{K}, l}(g_2)$.

Asymptotics.IsLittleOTVS.congr theorem

(h : f₁ =o[𝕜; l] g₁) (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) : f₂ =o[𝕜; l] g₂

Full source

theorem IsLittleOTVS.congr (h : f₁ =o[𝕜; l] g₁) (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
    f₂ =o[𝕜; l] g₂ :=
  h.congr' (univ_mem' hf) (univ_mem' hg)

Little-o Relation is Preserved Under Pointwise Equality

Informal description

Let $\mathbb{K}$ be a normed field, $\alpha$ a type, and $E$, $F$ topological vector spaces over $\mathbb{K}$ with zero elements. Let $l$ be a filter on $\alpha$, and $f_1, f_2 : \alpha \to E$, $g_1, g_2 : \alpha \to F$ be functions. If $f_1 = o_{\mathbb{K}, l}(g_1)$, and $f_1(x) = f_2(x)$ for all $x$, and $g_1(x) = g_2(x)$ for all $x$, then $f_2 = o_{\mathbb{K}, l}(g_2)$.

Asymptotics.IsLittleOTVS.congr_left theorem

(h : f₁ =o[𝕜; l] g) (hf : ∀ x, f₁ x = f₂ x) : f₂ =o[𝕜; l] g

Full source

theorem IsLittleOTVS.congr_left (h : f₁ =o[𝕜; l] g) (hf : ∀ x, f₁ x = f₂ x) : f₂ =o[𝕜; l] g :=
  h.congr hf fun _ => rfl

Left Congruence Property of Little-o Relation in Topological Vector Spaces

Informal description

Let $\mathbb{K}$ be a normed field, $\alpha$ a type, and $E$, $F$ topological vector spaces over $\mathbb{K}$ with zero elements. Let $l$ be a filter on $\alpha$, and $f_1, f_2 : \alpha \to E$, $g : \alpha \to F$ be functions. If $f_1 = o_{\mathbb{K}, l}(g)$ and $f_1(x) = f_2(x)$ for all $x$, then $f_2 = o_{\mathbb{K}, l}(g)$.

Asymptotics.IsLittleOTVS.congr_right theorem

(h : f =o[𝕜; l] g₁) (hg : ∀ x, g₁ x = g₂ x) : f =o[𝕜; l] g₂

Full source

theorem IsLittleOTVS.congr_right (h : f =o[𝕜; l] g₁) (hg : ∀ x, g₁ x = g₂ x) : f =o[𝕜; l] g₂ :=
  h.congr (fun _ => rfl) hg

Right Congruence Property of Little-o Relation in Topological Vector Spaces

Informal description

Let $\mathbb{K}$ be a normed field, $\alpha$ a type, and $E$, $F$ topological vector spaces over $\mathbb{K}$ with zero elements. Let $l$ be a filter on $\alpha$, and $f : \alpha \to E$, $g_1, g_2 : \alpha \to F$ be functions. If $f = o_{\mathbb{K}, l}(g_1)$ and $g_1(x) = g_2(x)$ for all $x$, then $f = o_{\mathbb{K}, l}(g_2)$.

Asymptotics.IsLittleOTVS.trans theorem

{k : α → G} (hfg : f =o[𝕜; l] g) (hgk : g =o[𝕜; l] k) : f =o[𝕜; l] k

Full source

@[trans]
theorem IsLittleOTVS.trans {k : α → G} (hfg : f =o[𝕜; l] g) (hgk : g =o[𝕜; l] k) :
    f =o[𝕜; l] k := by
  intros U hU
  obtain ⟨V, hV0, hV⟩ := hfg U hU
  obtain ⟨W, hW0, hW⟩ := hgk V hV0
  refine ⟨W, hW0, fun ε hε => ?_⟩
  filter_upwards [hV ε hε, hW 1 one_ne_zero] with a hfga hgka
  refine hfga.trans ?_
  gcongr
  simpa using hgka

Transitivity of Asymptotic Domination in Topological Vector Spaces

Informal description

Let $\mathbb{K}$ be a normed field, and let $E$, $F$, and $G$ be topological vector spaces over $\mathbb{K}$. Given functions $f : \alpha \to E$, $g : \alpha \to F$, and $k : \alpha \to G$, and a filter $l$ on $\alpha$, if $f$ is asymptotically dominated by $g$ (denoted $f = o_{\mathbb{K}, l}(g)$) and $g$ is asymptotically dominated by $k$ (denoted $g = o_{\mathbb{K}, l}(k)$), then $f$ is asymptotically dominated by $k$ (i.e., $f = o_{\mathbb{K}, l}(k)$).

Asymptotics.transIsLittleOTVSIsLittleOTVS instance

: @Trans (α → E) (α → F) (α → G) (· =o[𝕜; l] ·) (· =o[𝕜; l] ·) (· =o[𝕜; l] ·)

Full source

instance transIsLittleOTVSIsLittleOTVS :
    @Trans (α → E) (α → F) (α → G) (· =o[𝕜; l] ·) (· =o[𝕜; l] ·) (· =o[𝕜; l] ·) where
  trans := IsLittleOTVS.trans

Transitivity of Little-o in Topological Vector Spaces

Informal description

The relation $\cdot = o_{\mathbb{K}, l}(\cdot)$ on functions from $\alpha$ to topological vector spaces over a normed field $\mathbb{K}$ is transitive. That is, for functions $f : \alpha \to E$, $g : \alpha \to F$, and $k : \alpha \to G$, if $f = o_{\mathbb{K}, l}(g)$ and $g = o_{\mathbb{K}, l}(k)$, then $f = o_{\mathbb{K}, l}(k)$.

Filter.HasBasis.isLittleOTVS_iff theorem

 {ιE ιF : Sort*} {pE : ιE → Prop} {pF : ιF → Prop} {sE : ιE → Set E} {sF : ιF → Set F} (hE : HasBasis (𝓝 (0 : E)) pE sE)
  (hF : HasBasis (𝓝 (0 : F)) pF sF) :
  f =o[𝕜; l] g ↔ ∀ i, pE i → ∃ j, pF j ∧ ∀ ε ≠ (0 : ℝ≥0), ∀ᶠ x in l, egauge 𝕜 (sE i) (f x) ≤ ε * egauge 𝕜 (sF j) (g x)

Full source

theorem _root_.Filter.HasBasis.isLittleOTVS_iff {ιE ιF : Sort*} {pE : ιE → Prop} {pF : ιF → Prop}
    {sE : ιE → Set E} {sF : ιF → Set F} (hE : HasBasis (𝓝 (0 : E)) pE sE)
    (hF : HasBasis (𝓝 (0 : F)) pF sF) :
    f =o[𝕜; l] gf =o[𝕜; l] g ↔ ∀ i, pE i → ∃ j, pF j ∧ ∀ ε ≠ (0 : ℝ≥0),
      ∀ᶠ x in l, egauge 𝕜 (sE i) (f x) ≤ ε * egauge 𝕜 (sF j) (g x) := by
  refine (hE.forall_iff ?_).trans <| forall₂_congr fun _ _ ↦ hF.exists_iff ?_
  · rintro s t hsub ⟨V, hV₀, hV⟩
    exact ⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x ↦ le_trans <| egauge_anti _ hsub _⟩
  · refine fun s t hsub h ε hε ↦ (h ε hε).mono fun x hx ↦ hx.trans ?_
    gcongr

Characterization of Little-o Relation via Filter Bases in Topological Vector Spaces

Informal description

Let $\mathbb{K}$ be a normed field, and let $E$ and $F$ be topological vector spaces over $\mathbb{K}$. Suppose the neighborhood filters of zero in $E$ and $F$ have bases indexed by types $\iota_E$ and $\iota_F$ with predicates $p_E$, $p_F$ and sets $s_E$, $s_F$ respectively. For functions $f : \alpha \to E$ and $g : \alpha \to F$, and a filter $l$ on $\alpha$, the following are equivalent: 1. $f$ is asymptotically dominated by $g$ (denoted $f = o_{\mathbb{K}, l}(g)$) 2. For every index $i$ with $p_E(i)$, there exists an index $j$ with $p_F(j)$ such that for all $\varepsilon > 0$ in $\mathbb{R}_{\geq 0}$, the inequality \[ \text{egauge}_{\mathbb{K}}(s_E(i), f(x)) \leq \varepsilon \cdot \text{egauge}_{\mathbb{K}}(s_F(j), g(x)) \] holds for all $x$ in $l$ eventually. Here $\text{egauge}_{\mathbb{K}}(U, y) = \inf\{\|c\| \mid c \in \mathbb{K}, y \in c \cdot U\}$ is the Minkowski functional.

Asymptotics.isLittleOTVS_iff_smallSets theorem

 :
  f =o[𝕜; l] g ↔ ∀ U ∈ 𝓝 0, ∀ᶠ V in (𝓝 0).smallSets, ∀ ε ≠ (0 : ℝ≥0), ∀ᶠ x in l, egauge 𝕜 U (f x) ≤ ε * egauge 𝕜 V (g x)

Full source

theorem isLittleOTVS_iff_smallSets :
    f =o[𝕜; l] gf =o[𝕜; l] g ↔ ∀ U ∈ 𝓝 0, ∀ᶠ V in (𝓝 0).smallSets, ∀ ε ≠ (0 : ℝ≥0),
      ∀ᶠ x in l, egauge 𝕜 U (f x) ≤ ε * egauge 𝕜 V (g x) :=
  forall₂_congr fun U hU ↦ .symm <| eventually_smallSets' fun V₁ V₂ hV hV₂ ε hε ↦
    (hV₂ ε hε).mono fun x hx ↦ hx.trans <| by gcongr

Characterization of Little-o in Topological Vector Spaces via Small Sets

Informal description

Let $\mathbb{K}$ be a normed field, $E$ and $F$ be topological vector spaces over $\mathbb{K}$, and $l$ be a filter on a type $\alpha$. For functions $f : \alpha \to E$ and $g : \alpha \to F$, the following are equivalent: 1. $f$ is asymptotically dominated by $g$ with respect to $\mathbb{K}$ and $l$ (denoted $f = o_{\mathbb{K}, l}(g)$). 2. For every neighborhood $U$ of zero in $E$ and for every neighborhood $V$ in a neighborhood basis of zero in $F$, there exists $\varepsilon > 0$ such that eventually for all $x$ in $l$, the Minkowski functional satisfies $\text{egauge}_{\mathbb{K}, U}(f(x)) \leq \varepsilon \cdot \text{egauge}_{\mathbb{K}, V}(g(x))$. Here, $\text{egauge}_{\mathbb{K}, U}(y) = \inf \{ \|c\| \mid c \in \mathbb{K}, y \in c \cdot U \}$ is the Minkowski functional of $U$ at $y$.

Asymptotics.isLittleOTVS_map theorem

{k : β → α} {l : Filter β} : f =o[𝕜; map k l] g ↔ (f ∘ k) =o[𝕜; l] (g ∘ k)

Full source

@[simp]
theorem isLittleOTVS_map {k : β → α} {l : Filter β} :
    f =o[𝕜; map k l] gf =o[𝕜; map k l] g ↔ (f ∘ k) =o[𝕜; l] (g ∘ k) := by
  simp [IsLittleOTVS]

Composition Preserves Little-o Relation in Topological Vector Spaces

Informal description

Let $\mathbb{K}$ be a normed field, $\alpha$ and $\beta$ be types, $E$ and $F$ be topological vector spaces over $\mathbb{K}$ with zero elements, $f : \alpha \to E$ and $g : \alpha \to F$ be functions, and $l$ be a filter on $\beta$. For any function $k : \beta \to \alpha$, the following are equivalent: 1. $f$ is asymptotically dominated by $g$ with respect to the filter $\text{map } k \ l$ on $\alpha$, denoted $f = o_{\mathbb{K}, \text{map } k \ l}(g)$. 2. The composition $f \circ k$ is asymptotically dominated by $g \circ k$ with respect to the filter $l$ on $\beta$, denoted $(f \circ k) = o_{\mathbb{K}, l}(g \circ k)$. Here, $f = o_{\mathbb{K}, l}(g)$ means that for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $F$ such that for every $\varepsilon > 0$, the inequality $\text{egauge}_{\mathbb{K}, U}(f(x)) \leq \varepsilon \cdot \text{egauge}_{\mathbb{K}, V}(g(x))$ holds for all $x$ in $l$ eventually.

Asymptotics.IsLittleOTVS.mono theorem

(hf : f =o[𝕜; l₁] g) (h : l₂ ≤ l₁) : f =o[𝕜; l₂] g

Full source

lemma IsLittleOTVS.mono (hf : f =o[𝕜; l₁] g) (h : l₂ ≤ l₁) : f =o[𝕜; l₂] g :=
  fun U hU => let ⟨V, hV0, hV⟩ := hf U hU; ⟨V, hV0, fun ε hε => (hV ε hε).filter_mono h⟩

Monotonicity of Little-o Relation in Topological Vector Spaces with Respect to Filters

Informal description

Let $\mathbb{K}$ be a normed field, and let $E$ and $F$ be topological vector spaces over $\mathbb{K}$. Given two functions $f : \alpha \to E$ and $g : \alpha \to F$, and filters $l_1$ and $l_2$ on $\alpha$, if $f = o_{\mathbb{K}, l_1}(g)$ and $l_2 \leq l_1$ (i.e., $l_2$ is finer than $l_1$), then $f = o_{\mathbb{K}, l_2}(g)$. Here, $f = o_{\mathbb{K}, l}(g)$ means that for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $F$ such that the Minkowski functional $\text{egauge}_{\mathbb{K}, U}(f(x))$ is asymptotically dominated by $\text{egauge}_{\mathbb{K}, V}(g(x))$ as $x$ tends to $l$.

Asymptotics.IsLittleOTVS.comp_tendsto theorem

{k : β → α} {lb : Filter β} (h : f =o[𝕜; l] g) (hk : Tendsto k lb l) : (f ∘ k) =o[𝕜; lb] (g ∘ k)

Full source

lemma IsLittleOTVS.comp_tendsto {k : β → α} {lb : Filter β} (h : f =o[𝕜; l] g)
    (hk : Tendsto k lb l) : (f ∘ k) =o[𝕜; lb] (g ∘ k) :=
  isLittleOTVS_map.mp (h.mono hk)

Composition with Tendsto Preserves Little-o Relation in Topological Vector Spaces

Informal description

Let $\mathbb{K}$ be a normed field, $E$ and $F$ be topological vector spaces over $\mathbb{K}$, and $f : \alpha \to E$ and $g : \alpha \to F$ be functions. Given a filter $l$ on $\alpha$, if $f = o_{\mathbb{K}, l}(g)$ and $k : \beta \to \alpha$ is a function such that $k$ tends to $l$ along a filter $lb$ on $\beta$, then the composition $f \circ k$ is $o_{\mathbb{K}, lb}(g \circ k)$. Here, $f = o_{\mathbb{K}, l}(g)$ means that for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $F$ such that the Minkowski functional $\text{egauge}_{\mathbb{K}, U}(f(x))$ is asymptotically dominated by $\text{egauge}_{\mathbb{K}, V}(g(x))$ as $x$ tends to $l$.

Asymptotics.isLittleOTVS_sup theorem

: f =o[𝕜; l₁ ⊔ l₂] g ↔ f =o[𝕜; l₁] g ∧ f =o[𝕜; l₂] g

Full source

lemma isLittleOTVS_sup : f =o[𝕜; l₁ ⊔ l₂] gf =o[𝕜; l₁ ⊔ l₂] g ↔ f =o[𝕜; l₁] g ∧ f =o[𝕜; l₂] g := by
  simp only [isLittleOTVS_iff_smallSets, ← forall_and, ← eventually_and, eventually_sup]

Little-o relation splits over filter supremum in topological vector spaces

Informal description

Let $\mathbb{K}$ be a normed field, $E$ and $F$ be topological vector spaces over $\mathbb{K}$, and $l_1$, $l_2$ be filters on a type $\alpha$. For functions $f : \alpha \to E$ and $g : \alpha \to F$, the relation $f = o_{\mathbb{K}, l_1 \sqcup l_2}(g)$ holds if and only if both $f = o_{\mathbb{K}, l_1}(g)$ and $f = o_{\mathbb{K}, l_2}(g)$ hold. Here, $f = o_{\mathbb{K}, l}(g)$ means that for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $F$ such that $\text{egauge}_{\mathbb{K}, U}(f(x)) \leq \varepsilon \cdot \text{egauge}_{\mathbb{K}, V}(g(x))$ holds for all $x$ in $l$ eventually, where $\text{egauge}_{\mathbb{K}, U}(y) = \inf \{ \|c\| \mid c \in \mathbb{K}, y \in c \cdot U \}$ is the Minkowski functional of $U$ at $y$.

Asymptotics.IsLittleOTVS.sup theorem

(hf₁ : f =o[𝕜; l₁] g) (hf₂ : f =o[𝕜; l₂] g) : f =o[𝕜; l₁ ⊔ l₂] g

Full source

lemma IsLittleOTVS.sup (hf₁ : f =o[𝕜; l₁] g) (hf₂ : f =o[𝕜; l₂] g) : f =o[𝕜; l₁ ⊔ l₂] g :=
  isLittleOTVS_sup.mpr ⟨hf₁, hf₂⟩

Little-o relation is preserved under filter supremum in topological vector spaces

Informal description

Let $\mathbb{K}$ be a normed field, $E$ and $F$ be topological vector spaces over $\mathbb{K}$, and $l_1$, $l_2$ be filters on a type $\alpha$. For functions $f : \alpha \to E$ and $g : \alpha \to F$, if $f = o_{\mathbb{K}, l_1}(g)$ and $f = o_{\mathbb{K}, l_2}(g)$, then $f = o_{\mathbb{K}, l_1 \sqcup l_2}(g)$. Here, $f = o_{\mathbb{K}, l}(g)$ means that for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $F$ such that the Minkowski functional $\text{egauge}_{\mathbb{K}, U}(f(x))$ is asymptotically dominated by $\text{egauge}_{\mathbb{K}, V}(g(x))$ as $x$ tends to $l$.

Asymptotics.IsLittleOTVS.zero theorem

(g : α → F) (l : Filter α) : (0 : α → E) =o[𝕜; l] g

Full source

@[simp]
lemma IsLittleOTVS.zero (g : α → F) (l : Filter α) : (0 : α → E) =o[𝕜; l] g := by
  intros U hU
  simpa [egauge_zero_right _ (Filter.nonempty_of_mem hU)] using ⟨univ, by simp⟩

Zero Function is Little-o of Any Function in Topological Vector Spaces

Informal description

For any function $g : \alpha \to F$ and any filter $l$ on $\alpha$, the zero function $0 : \alpha \to E$ is asymptotically dominated by $g$ with respect to the normed field $\mathbb{K}$ and filter $l$, denoted as $0 = o_{\mathbb{K}, l}(g)$. This means that for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $F$ such that the Minkowski functional $\text{egauge}_{\mathbb{K}, U}(0) \leq \varepsilon \cdot \text{egauge}_{\mathbb{K}, V}(g(x))$ holds for all $x$ in $l$ eventually.

Asymptotics.isLittleOTVS_insert theorem

 [TopologicalSpace α] {x : α} {s : Set α} (h : f x = 0) : f =o[𝕜; 𝓝[insert x s] x] g ↔ f =o[𝕜; 𝓝[s] x] g

Full source

lemma isLittleOTVS_insert [TopologicalSpace α] {x : α} {s : Set α} (h : f x = 0) :
    f =o[𝕜; 𝓝[insert x s] x] gf =o[𝕜; 𝓝[insert x s] x] g ↔ f =o[𝕜; 𝓝[s] x] g := by
  rw [nhdsWithin_insert, isLittleOTVS_sup, and_iff_right]
  exact .congr' (.zero g _) h.symm .rfl

Asymptotic Little-o Relation at Inserted Point iff Within Original Set

Informal description

Let $\alpha$ be a topological space, $x \in \alpha$, and $s \subseteq \alpha$. For functions $f : \alpha \to E$ and $g : \alpha \to F$ where $E$ and $F$ are topological vector spaces over a normed field $\mathbb{K}$, if $f(x) = 0$, then $f$ is asymptotically dominated by $g$ at $x$ within $\{x\} \cup s$ if and only if $f$ is asymptotically dominated by $g$ at $x$ within $s$. Here, $f = o_{\mathbb{K}, \mathcal{N}_A(x)}(g)$ means that for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $F$ such that $\text{egauge}_{\mathbb{K}, U}(f(y)) \leq \varepsilon \cdot \text{egauge}_{\mathbb{K}, V}(g(y))$ for all $y$ in some neighborhood of $x$ within $A$, where $\text{egauge}_{\mathbb{K}, U}(y) = \inf \{ \|c\| \mid c \in \mathbb{K}, y \in c \cdot U \}$ is the Minkowski functional of $U$ at $y$.

Asymptotics.IsLittleOTVS.insert theorem

 [TopologicalSpace α] {x : α} {s : Set α} (h : f =o[𝕜; 𝓝[s] x] g) (hf : f x = 0) : f =o[𝕜; 𝓝[insert x s] x] g

Full source

lemma IsLittleOTVS.insert [TopologicalSpace α] {x : α} {s : Set α}
    (h : f =o[𝕜; 𝓝[s] x] g) (hf : f x = 0) :
    f =o[𝕜; 𝓝[insert x s] x] g :=
  (isLittleOTVS_insert hf).2 h

Extension of Little-o Relation to Inserted Point in Topological Vector Spaces

Informal description

Let $\alpha$ be a topological space, $x \in \alpha$, and $s \subseteq \alpha$. For functions $f : \alpha \to E$ and $g : \alpha \to F$ where $E$ and $F$ are topological vector spaces over a normed field $\mathbb{K}$, if $f$ is asymptotically dominated by $g$ at $x$ within $s$ (i.e., $f = o_{\mathbb{K}, \mathcal{N}_s(x)}(g)$) and $f(x) = 0$, then $f$ is also asymptotically dominated by $g$ at $x$ within $\{x\} \cup s$. Here, $f = o_{\mathbb{K}, \mathcal{N}_A(x)}(g)$ means that for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $F$ such that $\text{egauge}_{\mathbb{K}, U}(f(y)) \leq \varepsilon \cdot \text{egauge}_{\mathbb{K}, V}(g(y))$ for all $y$ in some neighborhood of $x$ within $A$, where $\text{egauge}_{\mathbb{K}, U}(y) = \inf \{ \|c\| \mid c \in \mathbb{K}, y \in c \cdot U \}$ is the Minkowski functional of $U$ at $y$.

Asymptotics.IsLittleOTVS.bot theorem

: f =o[𝕜; ⊥] g

Full source

@[simp]
lemma IsLittleOTVS.bot : f =o[𝕜; ⊥] g :=
  fun u hU => ⟨univ, by simp⟩

Trivial Filter Implies Little-o Relation in Topological Vector Spaces

Informal description

For any functions $f$ and $g$ mapping into topological vector spaces over a normed field $\mathbb{K}$, the relation $f = o_{\mathbb{K}, \bot}(g)$ holds, where $\bot$ denotes the bottom filter. This means that $f$ is asymptotically dominated by $g$ with respect to the trivial filter.

Asymptotics.IsLittleOTVS.add theorem

 [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {f₁ f₂ : α → E} {g : α → F} {l : Filter α} (h₁ : f₁ =o[𝕜; l] g)
  (h₂ : f₂ =o[𝕜; l] g) : (f₁ + f₂) =o[𝕜; l] g

Full source

theorem IsLittleOTVS.add [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
    {f₁ f₂ : α → E} {g : α → F} {l : Filter α}
    (h₁ : f₁ =o[𝕜; l] g) (h₂ : f₂ =o[𝕜; l] g) : (f₁ + f₂) =o[𝕜; l] g := by
  rw [(nhds_basis_balanced 𝕜 E).add_self.isLittleOTVS_iff (basis_sets _)]
  rintro U ⟨hU, hUb⟩
  rcases ((h₁.eventually_smallSets U hU).and (h₂.eventually_smallSets U hU)).exists_mem_of_smallSets
    with ⟨V, hV, hVf₁, hVf₂⟩
  refine ⟨V, hV, fun ε hε ↦ ?_⟩
  filter_upwards [hVf₁ ε hε, hVf₂ ε hε] with x hx₁ hx₂
  exact (egauge_add_add_le hUb hUb _ _).trans (max_le hx₁ hx₂)

Sum of Little-o Functions is Little-o in Topological Vector Spaces

Informal description

Let $\mathbb{K}$ be a normed field, and let $E$ and $F$ be topological vector spaces over $\mathbb{K}$ such that $E$ is a topological additive group and the scalar multiplication $\mathbb{K} \times E \to E$ is continuous. For functions $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$, and a filter $l$ on $\alpha$, if $f_1 = o_{\mathbb{K}, l}(g)$ and $f_2 = o_{\mathbb{K}, l}(g)$, then the sum $f_1 + f_2$ is also $o_{\mathbb{K}, l}(g)$. Here, $f = o_{\mathbb{K}, l}(g)$ means that for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $F$ such that $\text{egauge}_{\mathbb{K}, U}(f(x)) \leq \varepsilon \cdot \text{egauge}_{\mathbb{K}, V}(g(x))$ for all $x$ in $l$ eventually, where $\text{egauge}_{\mathbb{K}, U}(y) = \inf \{ \|c\| \mid c \in \mathbb{K}, y \in c \cdot U \}$ is the Minkowski functional of $U$ at $y$.

Asymptotics.IsLittleOTVS.smul_left theorem

(h : f =o[𝕜; l] g) (c : α → 𝕜) : (fun x ↦ c x • f x) =o[𝕜; l] (fun x ↦ c x • g x)

Full source

protected lemma IsLittleOTVS.smul_left (h : f =o[𝕜; l] g) (c : α → 𝕜) :
    (fun x ↦ c x • f x) =o[𝕜; l] (fun x ↦ c x • g x) := by
  unfold IsLittleOTVS at *
  peel h with U hU V hV ε hε x hx
  rw [egauge_smul_right, egauge_smul_right, mul_left_comm]
  · gcongr
  all_goals exact fun _ ↦ Filter.nonempty_of_mem ‹_›

Scalar Multiplication Preserves Little-o Relation in Topological Vector Spaces

Informal description

Let $\mathbb{K}$ be a normed field, and let $E$ and $F$ be topological vector spaces over $\mathbb{K}$. Given a filter $l$ on a type $\alpha$, functions $f, g : \alpha \to E$, and a scalar-valued function $c : \alpha \to \mathbb{K}$, if $f$ is asymptotically dominated by $g$ (denoted $f = o_{\mathbb{K}, l}(g)$), then the scaled function $x \mapsto c(x) \cdot f(x)$ is asymptotically dominated by $x \mapsto c(x) \cdot g(x)$ (i.e., $(c \cdot f) = o_{\mathbb{K}, l}(c \cdot g)$). Here, $f = o_{\mathbb{K}, l}(g)$ means that for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $F$ such that $\text{egauge}_{\mathbb{K}, U}(f(x)) \leq \varepsilon \cdot \text{egauge}_{\mathbb{K}, V}(g(x))$ for all $x$ in $l$ eventually, where $\text{egauge}_{\mathbb{K}, U}(y) = \inf \{ \|c\| \mid c \in \mathbb{K}, y \in c \cdot U \}$ is the Minkowski functional of $U$ at $y$.

Asymptotics.IsLittleOTVS.tendsto_inv_smul theorem

 [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E} (h : g =o[𝕜; l] f) : Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0)

Full source

lemma IsLittleOTVS.tendsto_inv_smul [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E}
    (h : g =o[𝕜; l] f) : Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0) := by
  rw [← isLittleOTVS_one (𝕜 := 𝕜)]
  intro U hU
  rcases h.smul_left f⁻¹ U hU with ⟨V, hV₀, hV⟩
  refine ⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x hx ↦ hx.trans ?_⟩
  by_cases hx₀ : f x = 0 <;> simp [hx₀, egauge_zero_right _ (Filter.nonempty_of_mem hV₀)]

Convergence of Scaled Inverse for Little-o in Topological Vector Spaces

Informal description

Let $\mathbb{K}$ be a normed field, $E$ a topological vector space over $\mathbb{K}$ with continuous scalar multiplication, and $l$ a filter on a type $\alpha$. Given functions $f : \alpha \to \mathbb{K}$ and $g : \alpha \to E$, if $g$ is asymptotically dominated by $f$ (denoted $g = o_{\mathbb{K}, l}(f)$), then the function $x \mapsto (f(x))^{-1} \cdot g(x)$ tends to zero along the filter $l$. Here, $g = o_{\mathbb{K}, l}(f)$ means that for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $\mathbb{K}$ such that $\text{egauge}_{\mathbb{K}, U}(g(x)) \leq \varepsilon \cdot \text{egauge}_{\mathbb{K}, V}(f(x))$ for all $x$ in $l$ eventually, where $\text{egauge}_{\mathbb{K}, U}(y) = \inf \{ \|c\| \mid c \in \mathbb{K}, y \in c \cdot U \}$ is the Minkowski functional of $U$ at $y$.

Asymptotics.isLittleOTVS_iff_tendsto_inv_smul theorem

 [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E} {l : Filter α} (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) :
  g =o[𝕜; l] f ↔ Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0)

Full source

lemma isLittleOTVS_iff_tendsto_inv_smul [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E} {l : Filter α}
    (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) :
    g =o[𝕜; l] fg =o[𝕜; l] f ↔ Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0) := by
  refine ⟨IsLittleOTVS.tendsto_inv_smul, fun h ↦ ?_⟩
  refine (((isLittleOTVS_one (𝕜 := 𝕜)).mpr h).smul_left f).congr' (h₀.mono fun x hx ↦ ?_) (by simp)
  by_cases h : f x = 0 <;> simp [h, hx]

Equivalence of Little-o and Scaled Inverse Convergence in Topological Vector Spaces

Informal description

Let $\mathbb{K}$ be a normed field, $E$ a topological vector space over $\mathbb{K}$ with continuous scalar multiplication, and $l$ a filter on a type $\alpha$. Given functions $f : \alpha \to \mathbb{K}$ and $g : \alpha \to E$ such that $g(x) = 0$ whenever $f(x) = 0$ for all $x$ in $l$ eventually, the following are equivalent: 1. $g$ is asymptotically dominated by $f$ (denoted $g = o_{\mathbb{K}, l}(f)$) 2. The function $x \mapsto (f(x))^{-1} \cdot g(x)$ tends to zero along the filter $l$. Here, $g = o_{\mathbb{K}, l}(f)$ means that for every neighborhood $U$ of zero in $E$, there exists a neighborhood $V$ of zero in $\mathbb{K}$ such that the Minkowski functional $\text{egauge}_{\mathbb{K}, U}(g(x)) \leq \varepsilon \cdot \text{egauge}_{\mathbb{K}, V}(f(x))$ for all $x$ in $l$ eventually.

Asymptotics.isLittleOTVS_iff_isLittleO theorem

{f : α → E} {g : α → F} {l : Filter α} : f =o[𝕜; l] g ↔ f =o[l] g

Full source

lemma isLittleOTVS_iff_isLittleO {f : α → E} {g : α → F} {l : Filter α} :
    f =o[𝕜; l] gf =o[𝕜; l] g ↔ f =o[l] g := by
  rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc : 1 < ‖c‖₊⟩
  have hc₀ : 0 < ‖c‖₊ := one_pos.trans hc
  simp only [isLittleO_iff, nhds_basis_ball.isLittleOTVS_iff nhds_basis_ball]
  refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ⟨1, one_pos, fun δ hδ ↦ ?_⟩⟩
  · rcases h ε hε with ⟨δ, hδ₀, hδ⟩
    lift ε to ℝ≥0 using hε.le; lift δ to ℝ≥0 using hδ₀.le; norm_cast at hε hδ₀
    filter_upwards [hδ (δ / ‖c‖₊) (div_pos hδ₀ hc₀).ne'] with x hx
    suffices (‖f x‖₊ / ε : ℝ≥0∞) ≤ ‖g x‖₊ by
      rw [← ENNReal.coe_div hε.ne'] at this
      rw [← div_le_iff₀' (NNReal.coe_pos.2 hε)]
      exact_mod_cast this
    calc
      (‖f x‖₊ / ε : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 ε) (f x) := div_le_egauge_ball 𝕜 _ _
      _ ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x) := hx
      _ ≤ (δ / ‖c‖₊) * (‖c‖₊ * ‖g x‖₊ / δ) := by
        gcongr
        exacts [ENNReal.coe_div_le, egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hδ₀)]
      _ = (δ / δ) * (‖c‖₊ / ‖c‖₊) * ‖g x‖₊ := by simp only [div_eq_mul_inv]; ring
      _ ≤ 1 * 1 * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
      _ = ‖g x‖₊ := by simp
  · filter_upwards [@h ↑(ε * δ / ‖c‖₊) (by positivity)] with x (hx : ‖f x‖₊ ≤ ε * δ / ‖c‖₊ * ‖g x‖₊)
    lift ε to ℝ≥0 using hε.le
    calc
      egauge 𝕜 (ball 0 ε) (f x) ≤ ‖c‖₊ * ‖f x‖₊ / ε :=
        egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hε)
      _ ≤ ‖c‖₊ * (↑(ε * δ / ‖c‖₊) * ‖g x‖₊) / ε := by gcongr; exact_mod_cast hx
      _ = (‖c‖₊ / ‖c‖₊) * (ε / ε) * δ * ‖g x‖₊ := by
        simp only [div_eq_mul_inv, ENNReal.coe_inv hc₀.ne', ENNReal.coe_mul]; ring
      _ ≤ 1 * 1 * δ * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
      _ = δ * ‖g x‖₊ := by simp
      _ ≤ δ * egauge 𝕜 (ball 0 1) (g x) := by gcongr; apply le_egauge_ball_one

Equivalence of Little-o Definitions in Normed Spaces: $f = o_{\mathbb{K}, l}(g) \leftrightarrow f = o_l(g)$

Informal description

Let $\mathbb{K}$ be a normed field, and let $E$ and $F$ be normed spaces over $\mathbb{K}$. For functions $f : \alpha \to E$ and $g : \alpha \to F$, and a filter $l$ on $\alpha$, the following are equivalent: 1. $f$ is asymptotically dominated by $g$ in the topological vector space sense (denoted $f = o_{\mathbb{K}, l}(g)$) 2. $f$ is asymptotically dominated by $g$ in the classical normed space sense (denoted $f = o_l(g)$)