English
Suppose ∀ᶠ x in l, g''(x) ≠ 0. Then f = O_l g'' iff the ratio of norms ‖f(x)‖/‖g''(x)‖ is bounded along l.
Русский
Пусть почти везде по l выполняется g''(x) ≠ 0. Тогда f = O_l g'' тогда как отношение норм ‖f(x)‖/‖g''(x)‖ ограничено вдоль l.
LaTeX
$$$ (\forall^{\!\!\!} x \in l, g''(x) \neq 0) \Rightarrow (f =O[l] g'' \iff IsBoundedUnder (\le) l (\|f(x)\|/\|g''(x)\|)). $$$
Lean4
theorem isBigO_const_iff {c : F''} :
(f'' =O[l] fun _x => c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (· ≤ ·) l fun x => ‖f'' x‖ :=
by
refine ⟨fun h => ⟨fun hc => isBigO_zero_right_iff.1 (by rwa [← hc]), h.isBoundedUnder_le⟩, ?_⟩
rintro ⟨hcf, hf⟩
rcases eq_or_ne c 0 with (hc | hc)
exacts [(hcf hc).trans_isBigO (isBigO_zero _ _), hf.isBigO_const hc]
