Asymptotics in a Topological Vector Space

This file defines Asymptotics.IsLittleOTVS and Asymptotics.IsBigOTVS as generalizations of Asymptotics.IsLittleO and Asymptotics.IsBigO 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)$ (resp., $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)))$ (resp, $\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 field. This is exactly the tradeoff we want in HasFDerivAtFilter, as there the base field is already chosen, and this removes the choice of norm being part of the statement.

These definitions were added to the library in order to migrate Fréchet derivatives from normed vector spaces to topological vector spaces. The definitions are 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 of Asymptotics.IsLittleOTVS, and Asymptotics.IsBigOTVS was defined in a similar manner.

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

• Add Asymptotics.IsThetaTVS and Asymptotics.IsEquivalentTVS.
• Prove equivalence of IsBigOTVS and IsBigO.
• Prove a version of Asymptotics.isBigO_One for IsBigOTVS.

structure 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] (l : Filter α) (f : α → E) (g : α → 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.

• exists_eventuallyLE_mul (U : Set E) : U ∈ nhds 0 → ∃ V ∈ nhds 0, ∀ (ε : NNReal), ε ≠ 0 → (fun (x : α) => egauge 𝕜 U (f x)) ≤ᶠ[l] fun (x : α) => ↑ε * egauge 𝕜 V (g x)

theorem Asymptotics.isLittleOTVS_iff (𝕜 : 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] (l : Filter α) (f : α → E) (g : α → F) : f =o[𝕜; l] g ↔ ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, ∀ (ε : NNReal), ε ≠ 0 → (fun (x : α) => egauge 𝕜 U (f x)) ≤ᶠ[l] fun (x : α) => ↑ε * egauge 𝕜 V (g x)

def Asymptotics.«term_=o[_;_]_» : Lean.TrailingParserDescr

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.

Equations

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

structure Asymptotics.IsBigOTVS (𝕜 : 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] (l : Filter α) (f : α → E) (g : α → F) : Prop

f =O[𝕜; l] g (IsBigOTVS 𝕜 l f g) is a generalization of f =O[l] g (IsBigO 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 𝕜, 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)) \le \operatorname{gauge}_{K, V} (g(x))$, where $\operatorname{gauge}_{K, U}(y) = \inf \{‖c‖ \mid y ∈ c • U\}$.

• exists_eventuallyLE (U : Set E) : U ∈ nhds 0 → ∃ V ∈ nhds 0, (fun (x : α) => egauge 𝕜 U (f x)) ≤ᶠ[l] fun (x : α) => egauge 𝕜 V (g x)

theorem Asymptotics.isBigOTVS_iff (𝕜 : 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] (l : Filter α) (f : α → E) (g : α → F) : f =O[𝕜; l] g ↔ ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, (fun (x : α) => egauge 𝕜 U (f x)) ≤ᶠ[l] fun (x : α) => egauge 𝕜 V (g x)

def Asymptotics.«term_=O[_;_]_» : Lean.TrailingParserDescr

f =O[𝕜; l] g (IsBigOTVS 𝕜 l f g) is a generalization of f =O[l] g (IsBigO 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 𝕜, 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)) \le \operatorname{gauge}_{K, V} (g(x))$, where $\operatorname{gauge}_{K, U}(y) = \inf \{‖c‖ \mid y ∈ c • U\}$.

Equations

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

theorem Asymptotics.isLittleOTVS_iff_tendsto_div {α : 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 α} : f =o[𝕜; l] g ↔ ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, Filter.Tendsto (fun (x : α) => egauge 𝕜 U (f x) / egauge 𝕜 V (g x)) l (nhds 0)

theorem Asymptotics.IsLittleOTVS.of_tendsto_div {α : 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 α} : (∀ U ∈ nhds 0, ∃ V ∈ nhds 0, Filter.Tendsto (fun (x : α) => egauge 𝕜 U (f x) / egauge 𝕜 V (g x)) l (nhds 0)) → f =o[𝕜; l] g

Alias of the reverse direction of Asymptotics.isLittleOTVS_iff_tendsto_div.

theorem Asymptotics.IsLittleOTVS.tendsto_div {α : 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 α} : f =o[𝕜; l] g → ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, Filter.Tendsto (fun (x : α) => egauge 𝕜 U (f x) / egauge 𝕜 V (g x)) l (nhds 0)

Alias of the forward direction of Asymptotics.isLittleOTVS_iff_tendsto_div.

theorem Asymptotics.IsLittleOTVS.exists_eventuallyLE_mul_ennreal {α : 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 : f =o[𝕜; l] g) {U : Set E} (hU : U ∈ nhds 0) : ∃ V ∈ nhds 0, ∀ (ε : ENNReal), ε ≠ 0 → (fun (x : α) => egauge 𝕜 U (f x)) ≤ᶠ[l] fun (x : α) => ε * egauge 𝕜 V (g x)

A version of IsLittleOTVS.exists_eventuallyLE_mul where ε is quantified over ℝ≥0∞ instead of ℝ≥0.

theorem Asymptotics.isLittleOTVS_congr {α : 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₁ f₂ : α → E} {g₁ g₂ : α → F} {l : Filter α} (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₁ =o[𝕜; l] g₁ ↔ f₂ =o[𝕜; l] g₂

theorem Asymptotics.IsLittleOTVS.congr' {α : 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₁ f₂ : α → E} {g₁ g₂ : α → F} {l : Filter α} (h : f₁ =o[𝕜; l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₂ =o[𝕜; l] g₂

A stronger version of IsLittleOTVS.congr that requires the functions only agree along the filter.

theorem Asymptotics.IsLittleOTVS.congr {α : 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₁ f₂ : α → E} {g₁ g₂ : α → F} {l : Filter α} (h : f₁ =o[𝕜; l] g₁) (hf : ∀ (x : α), f₁ x = f₂ x) (hg : ∀ (x : α), g₁ x = g₂ x) : f₂ =o[𝕜; l] g₂

theorem Asymptotics.IsLittleOTVS.congr_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₁ f₂ : α → E} {g : α → F} {l : Filter α} (h : f₁ =o[𝕜; l] g) (hf : ∀ (x : α), f₁ x = f₂ x) : f₂ =o[𝕜; l] g

theorem Asymptotics.IsLittleOTVS.congr_right {α : 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₁ g₂ : α → F} {l : Filter α} (h : f =o[𝕜; l] g₁) (hg : ∀ (x : α), g₁ x = g₂ x) : f =o[𝕜; l] g₂

theorem Asymptotics.IsLittleOTVS.isBigOTVS {α : 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] {l : Filter α} {f : α → E} {g : α → F} (h : f =o[𝕜; l] g) : f =O[𝕜; l] g

theorem Asymptotics.IsBigOTVS.trans {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G} (hfg : f =O[𝕜; l] g) (hgk : g =O[𝕜; l] k) : f =O[𝕜; l] k

instance Asymptotics.instTransIsBigOTVSIsBigOTVS {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} : Trans (IsBigOTVS 𝕜 l) (IsBigOTVS 𝕜 l) (IsBigOTVS 𝕜 l)

Equations

• Asymptotics.instTransIsBigOTVSIsBigOTVS = { trans := ⋯ }

theorem Asymptotics.IsLittleOTVS.trans_isBigOTVS {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G} (hfg : f =o[𝕜; l] g) (hgk : g =O[𝕜; l] k) : f =o[𝕜; l] k

instance Asymptotics.instTransIsLittleOTVSIsBigOTVS {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} : Trans (IsLittleOTVS 𝕜 l) (IsBigOTVS 𝕜 l) (IsLittleOTVS 𝕜 l)

Equations

• Asymptotics.instTransIsLittleOTVSIsBigOTVS = { trans := ⋯ }

theorem Asymptotics.IsBigOTVS.trans_isLittleOTVS {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G} (hfg : f =O[𝕜; l] g) (hgk : g =o[𝕜; l] k) : f =o[𝕜; l] k

instance Asymptotics.instTransIsBigOTVSIsLittleOTVS {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} : Trans (IsBigOTVS 𝕜 l) (IsLittleOTVS 𝕜 l) (IsLittleOTVS 𝕜 l)

Equations

• Asymptotics.instTransIsBigOTVSIsLittleOTVS = { trans := ⋯ }

theorem Asymptotics.IsLittleOTVS.trans {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G} (hfg : f =o[𝕜; l] g) (hgk : g =o[𝕜; l] k) : f =o[𝕜; l] k

instance Asymptotics.instTransIsLittleOTVSIsLittleOTVS {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} : Trans (IsLittleOTVS 𝕜 l) (IsLittleOTVS 𝕜 l) (IsLittleOTVS 𝕜 l)

Equations

• Asymptotics.instTransIsLittleOTVSIsLittleOTVS = { trans := ⋯ }

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] {l : Filter α} {f : α → E} {g : α → F} {ιE : Sort u_7} {ιF : Sort u_8} {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 =o[𝕜; l] g ↔ ∀ (i : ιE), pE i → ∃ (j : ιF), pF j ∧ ∀ (ε : NNReal), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ ↑ε * egauge 𝕜 (sF j) (g x)

theorem Filter.HasBasis.isBigOTVS_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] {l : Filter α} {f : α → E} {g : α → F} {ιE : Sort u_7} {ιF : Sort u_8} {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 =O[𝕜; l] g ↔ ∀ (i : ιE), pE i → ∃ (j : ιF), pF j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ egauge 𝕜 (sF j) (g x)

theorem Asymptotics.isLittleOTVS_iff_smallSets {α : 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] {l : Filter α} {f : α → E} {g : α → F} : f =o[𝕜; l] g ↔ ∀ U ∈ nhds 0, ∀ᶠ (V : Set F) in (nhds 0).smallSets, ∀ (ε : NNReal), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)

theorem Asymptotics.IsLittleOTVS.eventually_smallSets {α : 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] {l : Filter α} {f : α → E} {g : α → F} : f =o[𝕜; l] g → ∀ U ∈ nhds 0, ∀ᶠ (V : Set F) in (nhds 0).smallSets, ∀ (ε : NNReal), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)

Alias of the forward direction of Asymptotics.isLittleOTVS_iff_smallSets.

theorem Asymptotics.isBigOTVS_iff_smallSets {α : 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] {l : Filter α} {f : α → E} {g : α → F} : f =O[𝕜; l] g ↔ ∀ U ∈ nhds 0, ∀ᶠ (V : Set F) in (nhds 0).smallSets, ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)

theorem Asymptotics.IsBigOTVS.eventually_smallSets {α : 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] {l : Filter α} {f : α → E} {g : α → F} : f =O[𝕜; l] g → ∀ U ∈ nhds 0, ∀ᶠ (V : Set F) in (nhds 0).smallSets, ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)

Alias of the forward direction of Asymptotics.isBigOTVS_iff_smallSets.

@[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 β} : f =o[𝕜; Filter.map k l] g ↔ (f ∘ k) =o[𝕜; l] (g ∘ k)

@[simp]

theorem Asymptotics.isBigOTVS_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 β} : f =O[𝕜; Filter.map k l] g ↔ (f ∘ k) =O[𝕜; l] (g ∘ k)

theorem Asymptotics.IsLittleOTVS.mono {α : 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] {l₁ l₂ : Filter α} {f : α → E} {g : α → F} (hf : f =o[𝕜; l₁] g) (h : l₂ ≤ l₁) : f =o[𝕜; l₂] g

theorem Asymptotics.IsBigOTVS.mono {α : 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] {l₁ l₂ : Filter α} {f : α → E} {g : α → F} (hf : f =O[𝕜; l₁] g) (h : l₂ ≤ l₁) : f =O[𝕜; l₂] g

theorem Asymptotics.IsLittleOTVS.comp_tendsto {α : 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] {l : Filter α} {f : α → E} {g : α → F} {k : β → α} {lb : Filter β} (h : f =o[𝕜; l] g) (hk : Filter.Tendsto k lb l) : (f ∘ k) =o[𝕜; lb] (g ∘ k)

theorem Asymptotics.IsBigOTVS.comp_tendsto {α : 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] {l : Filter α} {f : α → E} {g : α → F} {k : β → α} {lb : Filter β} (h : f =O[𝕜; l] g) (hk : Filter.Tendsto k lb l) : (f ∘ k) =O[𝕜; lb] (g ∘ k)

theorem Asymptotics.isLittleOTVS_sup {α : 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] {l₁ l₂ : Filter α} {f : α → E} {g : α → F} : f =o[𝕜; l₁ ⊔ l₂] g ↔ f =o[𝕜; l₁] g ∧ f =o[𝕜; l₂] g

theorem Asymptotics.IsLittleOTVS.sup {α : 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] {l₁ l₂ : Filter α} {f : α → E} {g : α → F} (hf₁ : f =o[𝕜; l₁] g) (hf₂ : f =o[𝕜; l₂] g) : f =o[𝕜; l₁ ⊔ l₂] g

theorem ContinuousLinearMap.isBigOTVS_id {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] {l : Filter E} (f : E →L[𝕜] F) : ⇑f =O[𝕜; l] _root_.id

theorem ContinuousLinearMap.isBigOTVS_comp {α : 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] {l : Filter α} {f : α → E} (g : E →L[𝕜] F) : (⇑g ∘ f) =O[𝕜; l] f

theorem ContinuousLinearMap.isBigOTVS_fun_comp {α : 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] {l : Filter α} {f : α → E} (g : E →L[𝕜] F) : (fun (x : α) => g (f x)) =O[𝕜; l] f

@[simp]

theorem Asymptotics.IsLittleOTVS.zero {α : 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] (g : α → F) (l : Filter α) : 0 =o[𝕜; l] g

theorem Asymptotics.isLittleOTVS_insert {α : 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} [TopologicalSpace α] {x : α} {s : Set α} (h : f x = 0) : f =o[𝕜; nhdsWithin x (insert x s)] g ↔ f =o[𝕜; nhdsWithin x s] g

theorem Asymptotics.IsLittleOTVS.insert {α : 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} [TopologicalSpace α] {x : α} {s : Set α} (h : f =o[𝕜; nhdsWithin x s] g) (hf : f x = 0) : f =o[𝕜; nhdsWithin x (Insert.insert x s)] g

@[simp]

theorem Asymptotics.IsLittleOTVS.bot {α : 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} : f =o[𝕜; ⊥] g

theorem Asymptotics.IsLittleOTVS.prodMk {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} (hf : f =o[𝕜; l] k) (hg : g =o[𝕜; l] k) : (fun (x : α) => (f x, g x)) =o[𝕜; l] k

theorem Asymptotics.IsLittleOTVS.fst {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} {f : α → E × F} {g : α → G} (h : f =o[𝕜; l] g) : (fun (x : α) => (f x).1) =o[𝕜; l] g

theorem Asymptotics.IsLittleOTVS.snd {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} {f : α → E × F} {g : α → G} (h : f =o[𝕜; l] g) : (fun (x : α) => (f x).2) =o[𝕜; l] g

@[simp]

theorem Asymptotics.isLittleOTVS_prodMk_left {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} : (fun (x : α) => (f x, g x)) =o[𝕜; l] k ↔ f =o[𝕜; l] k ∧ g =o[𝕜; l] k

theorem Asymptotics.IsBigOTVS.prodMk {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} (hf : f =O[𝕜; l] k) (hg : g =O[𝕜; l] k) : (fun (x : α) => (f x, g x)) =O[𝕜; l] k

theorem Asymptotics.IsBigOTVS.fst {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} {f : α → E × F} {g : α → G} (h : f =O[𝕜; l] g) : (fun (x : α) => (f x).1) =O[𝕜; l] g

theorem Asymptotics.IsBigOTVS.snd {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} {f : α → E × F} {g : α → G} (h : f =O[𝕜; l] g) : (fun (x : α) => (f x).2) =O[𝕜; l] g

@[simp]

theorem Asymptotics.isBigOTVS_prodMk_left {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} : (fun (x : α) => (f x, g x)) =O[𝕜; l] k ↔ f =O[𝕜; l] k ∧ g =O[𝕜; l] k

theorem Asymptotics.IsLittleOTVS.add {α : 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] [ContinuousAdd 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

theorem Asymptotics.IsBigOTVS.add {α : 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] [ContinuousAdd 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

theorem Asymptotics.IsLittleOTVS.pi {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] {l : Filter α} {g : α → F} {ι : Type u_7} {E : ι → Type u_8} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {f : (i : ι) → α → E i} (h : ∀ (i : ι), f i =o[𝕜; l] g) : (fun (x : α) (i : ι) => f i x) =o[𝕜; l] g

theorem Asymptotics.IsLittleOTVS.proj {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] {l : Filter α} {g : α → F} {ι : Type u_7} {E : ι → Type u_8} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] {f : α → (i : ι) → E i} (h : f =o[𝕜; l] g) (i : ι) : (fun (x : α) => f x i) =o[𝕜; l] g

theorem Asymptotics.isLittleOTVS_pi {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] {l : Filter α} {g : α → F} {ι : Type u_7} {E : ι → Type u_8} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {f : α → (i : ι) → E i} : f =o[𝕜; l] g ↔ ∀ (i : ι), (fun (x : α) => f x i) =o[𝕜; l] g

theorem Asymptotics.IsBigOTVS.pi {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] {l : Filter α} {g : α → F} {ι : Type u_7} {E : ι → Type u_8} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {f : (i : ι) → α → E i} (h : ∀ (i : ι), f i =O[𝕜; l] g) : (fun (x : α) (i : ι) => f i x) =O[𝕜; l] g

theorem Asymptotics.IsBigOTVS.proj {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] {l : Filter α} {g : α → F} {ι : Type u_7} {E : ι → Type u_8} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] {f : α → (i : ι) → E i} (h : f =O[𝕜; l] g) (i : ι) : (fun (x : α) => f x i) =O[𝕜; l] g

theorem Asymptotics.isBigOTVS_pi {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] {l : Filter α} {g : α → F} {ι : Type u_7} {E : ι → Type u_8} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {f : α → (i : ι) → E i} : f =O[𝕜; l] g ↔ ∀ (i : ι), (fun (x : α) => f x i) =O[𝕜; l] g

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] {l : Filter α} {f : α → E} {g : α → F} (h : f =o[𝕜; l] g) (c : α → 𝕜) : (fun (x : α) => c x • f x) =o[𝕜; l] fun (x : α) => c x • g x

theorem Asymptotics.isLittleOTVS_one {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] {l : Filter α} {f : α → E} [ContinuousSMul 𝕜 E] : f =o[𝕜; l] 1 ↔ 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] {l : Filter α} [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E} (h : g =o[𝕜; l] f) : 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) : g =o[𝕜; l] f ↔ Filter.Tendsto (fun (x : α) => (f x)⁻¹ • g x) l (nhds 0)

theorem Asymptotics.Filter.Tendsto.isBigOTVS_one {α : Type u_1} (𝕜 : Type u_3) {E : Type u_4} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] {l : Filter α} {f : α → E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] {x : E} (h : Filter.Tendsto f l (nhds x)) : f =O[𝕜; l] fun (x : α) => 1

If f converges along l to a finite limit x, then f =O[𝕜, l] 1.

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 α} : f =o[𝕜; l] g ↔ 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 α} : f =o[𝕜; l] g → f =o[l] g

Alias of the forward direction of Asymptotics.isLittleOTVS_iff_isLittleO.

theorem Asymptotics.IsLittleO.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 → f =o[𝕜; l] g

Alias of the reverse direction of Asymptotics.isLittleOTVS_iff_isLittleO.