English
Analogous to LittleOTVS, but for the Big-OTVS relation; exhibiting a bound that is uniform across smallSets around the origin.
Русский
Аналогично LittleOTVS для BigOTVS: демонстрирует границу, однородную по малым множествам около нуля.
LaTeX
$$$\\text{IsBigOTVS}(\\\\mathfrak{k}, l, f, g) \\iff \\forall U \\in 𝓝(0_E), \\forall V \\in (𝓝(0_E)).smallSets, \\forall ε>0:\\; \\forallᶠ x \\in l, \\; egauge(\\\\mathfrak{k}, U, f(x)) \\le egauge(\\\\mathfrak{k}, V, g(x)) \\cdot ε.$$$
Lean4
theorem isBigOTVS_iff_smallSets :
f =O[𝕜; l] g ↔ ∀ U ∈ 𝓝 0, ∀ᶠ V in (𝓝 0).smallSets, ∀ᶠ x in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x) :=
(isBigOTVS_iff ..).trans <|
forall₂_congr fun U hU ↦ .symm <| eventually_smallSets' fun V₁ V₂ hV hV₂ ↦ hV₂.mono fun x hx ↦ hx.trans <| by gcongr
