# 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`.

source
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)

Instances For

source
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)
source
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.

Instances For

source
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)

Instances For

source
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)
source
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.

Instances For

source
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)
source
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`.

source
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`.

source
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`.

source
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₂
source
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.

source
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₂
source
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
source
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₂
source
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
source
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
source
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 := ⋯ }

source
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
source
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 := ⋯ }

source
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
source
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 := ⋯ }

source
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
source
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 := ⋯ }

source
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)
source
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)
source
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)
source
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`.

source
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)
source
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`.

source
@[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)
source
@[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)
source
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
source
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
source
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)
source
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)
source
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
source
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
source
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] id
source
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
source
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
source
@[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
source
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
source
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
source
@[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
source
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
source
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
source
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
source
@[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
source
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
source
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
source
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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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)
source
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)
source
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)
source
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`.

source
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
source
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`.

source
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`.