English
Let f, g, h be functions from α to a normed division ring 𝕜, and suppose f(x) ≠ 0 for x in a tail of α. Then (f(x) g(x)) =O[h(x)] if and only if g(x) =O[h(x)/f(x)].
Русский
Пусть f, g, h — функции из α в нормированном деликовом кольце 𝕜, и существует tail, где f(x) ≠ 0. Тогда (f(x) g(x)) =O[h(x)] тогда и только тогда, когда g(x) =O[h(x)/f(x)].
LaTeX
$$$ (f \\cdot g) =O_l h \\iff g =O_l \\left( x \\mapsto \\frac{h(x)}{f(x)} \\right) $ (при условии, что ∀ᶠ x, f(x) ≠ 0)$$
Lean4
theorem isBigO_mul_iff_isBigO_div {f g h : α → 𝕜} (hf : ∀ᶠ x in l, f x ≠ 0) :
(fun x ↦ f x * g x) =O[l] h ↔ g =O[l] (fun x ↦ h x / f x) :=
by
rw [isBigO_iff', isBigO_iff']
refine ⟨fun ⟨c, hc, H⟩ ↦ ⟨c, hc, ?_⟩, fun ⟨c, hc, H⟩ ↦ ⟨c, hc, ?_⟩⟩ <;>
· refine H.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_
rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]
