Asymptotics for locally convex topological vector spaces

We provide a characterization of IsBigOTVS and IsLittleOTVS in terms of continuous seminorms and families of seminorms.

Main results:

• PolynormableSpace.isBigOTVS_iff
• PolynormableSpace.isLittleOTVS_iff
• WithSeminorms.isBigOTVS_iff
• WithSeminorms.isLittleOTVS_iff

theorem Seminorm.isBigO_comp_iff {α : Type u_3} {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} {p : Seminorm 𝕜 E} {q : Seminorm 𝕜 F} : (⇑p ∘ f) =O[l] (⇑q ∘ g) ↔ ∃ (C : NNReal), ⇑p ∘ f ≤ᶠ[l] ⇑(C • q) ∘ g

theorem Seminorm.isLittleO_comp_iff {α : Type u_3} {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} {p : Seminorm 𝕜 E} {q : Seminorm 𝕜 F} : (⇑p ∘ f) =o[l] (⇑q ∘ g) ↔ ∀ (ε : NNReal), ε ≠ 0 → ⇑p ∘ f ≤ᶠ[l] ⇑(ε • q) ∘ g

theorem PolynormableSpace.isBigOTVS_iff_le {α : Type u_3} {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} [TopologicalSpace E] [TopologicalSpace F] [PolynormableSpace 𝕜 E] [PolynormableSpace 𝕜 F] : f =O[𝕜; l] g ↔ ∀ (p : Seminorm 𝕜 E), Continuous ⇑p → ∃ (q : Seminorm 𝕜 F), Continuous ⇑q ∧ ⇑p ∘ f ≤ᶠ[l] ⇑q ∘ g

theorem PolynormableSpace.isBigOTVS_iff {α : Type u_3} {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} [TopologicalSpace E] [TopologicalSpace F] [PolynormableSpace 𝕜 E] [PolynormableSpace 𝕜 F] : f =O[𝕜; l] g ↔ ∀ (p : Seminorm 𝕜 E), Continuous ⇑p → ∃ (q : Seminorm 𝕜 F), Continuous ⇑q ∧ (⇑p ∘ f) =O[l] (⇑q ∘ g)

theorem PolynormableSpace.isLittleOTVS_iff_le {α : Type u_3} {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} [TopologicalSpace E] [TopologicalSpace F] [PolynormableSpace 𝕜 E] [PolynormableSpace 𝕜 F] : f =o[𝕜; l] g ↔ ∀ (p : Seminorm 𝕜 E), Continuous ⇑p → ∃ (q : Seminorm 𝕜 F), Continuous ⇑q ∧ ∀ (ε : NNReal), ε ≠ 0 → ⇑p ∘ f ≤ᶠ[l] ⇑(ε • q) ∘ g

theorem PolynormableSpace.isLittleOTVS_iff {α : Type u_3} {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} [TopologicalSpace E] [TopologicalSpace F] [PolynormableSpace 𝕜 E] [PolynormableSpace 𝕜 F] : f =o[𝕜; l] g ↔ ∀ (p : Seminorm 𝕜 E), Continuous ⇑p → ∃ (q : Seminorm 𝕜 F), Continuous ⇑q ∧ (⇑p ∘ f) =o[l] (⇑q ∘ g)

theorem WithSeminorms.isBigOTVS_iff_le_continuous {ι : Type u_1} {α : Type u_3} {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} [TopologicalSpace E] [TopologicalSpace F] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) [PolynormableSpace 𝕜 F] : f =O[𝕜; l] g ↔ ∀ (i : ι), ∃ (q : Seminorm 𝕜 F), Continuous ⇑q ∧ ⇑(p i) ∘ f ≤ᶠ[l] ⇑q ∘ g

theorem WithSeminorms.isBigOTVS_iff_le {ι : Type u_1} {κ : Type u_2} {α : Type u_3} {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} [TopologicalSpace E] [TopologicalSpace F] {p : SeminormFamily 𝕜 E ι} {q : SeminormFamily 𝕜 F κ} (hp : WithSeminorms p) (hq : WithSeminorms q) : f =O[𝕜; l] g ↔ ∀ (i : ι), ∃ (s : Finset κ) (C : NNReal), ⇑(p i) ∘ f ≤ᶠ[l] ⇑(C • s.sup q) ∘ g

theorem WithSeminorms.isBigOTVS_iff {ι : Type u_1} {κ : Type u_2} {α : Type u_3} {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} [TopologicalSpace E] [TopologicalSpace F] {p : SeminormFamily 𝕜 E ι} {q : SeminormFamily 𝕜 F κ} (hp : WithSeminorms p) (hq : WithSeminorms q) : f =O[𝕜; l] g ↔ ∀ (i : ι), ∃ (s : Finset κ), (⇑(p i) ∘ f) =O[l] (⇑(s.sup q) ∘ g)

theorem WithSeminorms.isLittleOTVS_iff_le_continuous {ι : Type u_1} {α : Type u_3} {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} [TopologicalSpace E] [TopologicalSpace F] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) [PolynormableSpace 𝕜 F] : f =o[𝕜; l] g ↔ ∀ (i : ι), ∃ (q : Seminorm 𝕜 F), Continuous ⇑q ∧ ∀ (ε : NNReal), ε ≠ 0 → ⇑(p i) ∘ f ≤ᶠ[l] ⇑(ε • q) ∘ g

theorem WithSeminorms.isLittleOTVS_iff_le {ι : Type u_1} {κ : Type u_2} {α : Type u_3} {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} [TopologicalSpace E] [TopologicalSpace F] {p : SeminormFamily 𝕜 E ι} {q : SeminormFamily 𝕜 F κ} (hp : WithSeminorms p) (hq : WithSeminorms q) : f =o[𝕜; l] g ↔ ∀ (i : ι), ∃ (s : Finset κ), ∀ (ε : NNReal), ε ≠ 0 → ⇑(p i) ∘ f ≤ᶠ[l] ⇑(ε • s.sup q) ∘ g

theorem WithSeminorms.isLittleOTVS_iff {ι : Type u_1} {κ : Type u_2} {α : Type u_3} {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} [TopologicalSpace E] [TopologicalSpace F] {p : SeminormFamily 𝕜 E ι} {q : SeminormFamily 𝕜 F κ} (hp : WithSeminorms p) (hq : WithSeminorms q) : f =o[𝕜; l] g ↔ ∀ (i : ι), ∃ (s : Finset κ), (⇑(p i) ∘ f) =o[l] (⇑(s.sup q) ∘ g)