English
Let l be a filter on α, and f, g : α → 𝕜 with 𝕜 a NormedDivisionRing. If f/g tends to c along l and, eventually, g(x) = 0 implies f(x) = 0, then f is of order O with respect to g along l; i.e., there exists C > 0 such that ‖f(x)‖ ≤ C‖g(x)‖ for x in a tail of l.
Русский
Пусть l — фильтр на α, и функции f, g : α → 𝕜, где 𝕜 — нормированное делимое кольцо. Если f/ g стремится к некоторому c по l и если почти в конце существует условие g(x) = 0 ⇒ f(x) = 0, то f = O_l(g); то есть существует C > 0 такое, что ‖f(x)‖ ≤ C‖g(x)‖ на хвосте l.
LaTeX
$$$\\displaystyle \\text{Let } l \\text{ be a filter on } \\alpha, \\ f,g:\\alpha\\to \\mathbb{K} \\ (\\mathbb{K} \\text{ NormedDivisionRing}). \\\\ \\text{If } (f/g) \\to c \\text{ along } l \\text{ and } (\\forall \\text{ x } x \\text{ eventually in } l,\\ g(x)=0 \\Rightarrow f(x)=0), \\\\ \\text{then } f = O_l(g).$$$
Lean4
theorem isBigO_of_div_tendsto_nhds {α : Type*} {l : Filter α} {f g : α → 𝕜} (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) (c : 𝕜)
(H : Filter.Tendsto (f / g) l (𝓝 c)) : f =O[l] g :=
(isBigO_iff_div_isBoundedUnder hgf).2 <| H.norm.isBoundedUnder_le
