English
Another variant: from IsBigOWith c l u v and c≥0 derive existence of φ with bound and u = φ v.
Русский
Другой вариант: из IsBigOWith c l u v и c≥0 следует существование φ с ограничением и u = φ v.
LaTeX
$$$ IsBigOWith\\ c\\ l\\ u\\ v \\land (0 \\le c) \\Rightarrow \\Exists φ : α \\to 𝕜, (\\forallᶠ x in l, \\|φ x\\| ≤ c) ∧ u =ᶠ[l] φ \\cdot v $$$
Lean4
theorem isBigO_iff_div_isBoundedUnder {α : Type*} {l : Filter α} {f g : α → 𝕜} (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) :
f =O[l] g ↔ IsBoundedUnder (· ≤ ·) l fun x => ‖f x / g x‖ :=
by
refine ⟨div_isBoundedUnder_of_isBigO, fun h => ?_⟩
obtain ⟨c, hc⟩ := h
simp only [eventually_map, norm_div] at hc
refine IsBigO.of_bound c (hc.mp <| hgf.mono fun x hx₁ hx₂ => ?_)
by_cases hgx : g x = 0
· simp [hx₁ hgx, hgx]
· exact (div_le_iff₀ (norm_pos_iff.2 hgx)).mp hx₂
