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 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%A9chet_derivative#Generalization_to_topological_vector_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.

TODO

Use this to redefine HasFDerivAtFilter, as the base ring is already chosen there, and this removes the choice of norm being part of the statement.

def Asymptotics.IsLittleOTVS (𝕜 : Type u_1) {α : Type u_2} {E : Type u_3} {F : Type u_4} [NNNorm 𝕜] [TopologicalSpace E] [TopologicalSpace F] [Zero E] [Zero F] [SMul 𝕜 E] [SMul 𝕜 F] (f : α → E) (g : α → F) (l : Filter α) : Prop

IsLittleOTVS 𝕜 f g l is a generalization of f =o[l] g (IsLittleO f g l) 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.

Equations

• Asymptotics.IsLittleOTVS 𝕜 f g l = ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, ∀ (ε : NNReal), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)

theorem Filter.HasBasis.isLittleOTVS_iff {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] {ιE : Sort u_6} {ιF : Sort u_7} {pE : ιE → Prop} {pF : ιF → Prop} {sE : ιE → Set E} {sF : ιF → Set F} (hE : (nhds 0).HasBasis pE sE) (hF : (nhds 0).HasBasis pF sF) {f : α → E} {g : α → F} {l : Filter α} : Asymptotics.IsLittleOTVS 𝕜 f g l ↔ ∀ (i : ιE), pE i → ∃ (j : ιF), pF j ∧ ∀ (ε : NNReal), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ ↑ε * egauge 𝕜 (sF j) (g x)

@[simp]

theorem Asymptotics.isLittleOTVS_map {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] {f : α → E} {g : α → F} {k : β → α} {l : Filter β} : Asymptotics.IsLittleOTVS 𝕜 f g (Filter.map k l) ↔ Asymptotics.IsLittleOTVS 𝕜 (f ∘ k) (g ∘ k) l

theorem Asymptotics.IsLittleOTVS.smul_left {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} (h : Asymptotics.IsLittleOTVS 𝕜 f g l) (c : α → 𝕜) : Asymptotics.IsLittleOTVS 𝕜 (fun (x : α) => c x • f x) (fun (x : α) => c x • g x) l

theorem Asymptotics.isLittleOTVS_one {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] {f : α → E} {l : Filter α} : Asymptotics.IsLittleOTVS 𝕜 f 1 l ↔ Filter.Tendsto f l (nhds 0)

theorem Asymptotics.IsLittleOTVS.tendsto_inv_smul {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E} {l : Filter α} (h : Asymptotics.IsLittleOTVS 𝕜 g f l) : Filter.Tendsto (fun (x : α) => (f x)⁻¹ • g x) l (nhds 0)

theorem Asymptotics.isLittleOTVS_iff_tendsto_inv_smul {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E} {l : Filter α} (h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0) : Asymptotics.IsLittleOTVS 𝕜 g f l ↔ Filter.Tendsto (fun (x : α) => (f x)⁻¹ • g x) l (nhds 0)

theorem Asymptotics.isLittleOTVS_iff_isLittleO {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} : Asymptotics.IsLittleOTVS 𝕜 f g l ↔ f =o[l] g

theorem Asymptotics.isLittleOTVS.isLittleO {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} : Asymptotics.IsLittleOTVS 𝕜 f g l → f =o[l] g

Alias of the forward direction of Asymptotics.isLittleOTVS_iff_isLittleO.

theorem Asymptotics.IsLittle.isLittleOTVS {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} : f =o[l] g → Asymptotics.IsLittleOTVS 𝕜 f g l

Alias of the reverse direction of Asymptotics.isLittleOTVS_iff_isLittleO.