English
If ∀ᶠ x in l, g''(x) ≠ 0, then f = O_l g'' iff the ratio of norms is bounded: ‖f(x)‖/‖g''(x)‖ is bounded along l.
Русский
Пусть ∀ᶠ x в l, g''(x) ≠ 0. Тогда f = O_l g'' эквивалентно тому, что отношение норм ограничено вдоль l: ‖f(x)‖/‖g''(x)‖ ограничено.
LaTeX
$$$ (\forall^{\!\!} x \in l, g''(x) \neq 0) \Rightarrow (f =O[l] g'' \iff IsBoundedUnder (\le) l (\|f(x)\|/\|g''(x)\|)). $$$
Lean4
/-- `(fun x ↦ c) =O[l] f` if and only if `f` is bounded away from zero. -/
theorem isBigO_const_left_iff_pos_le_norm {c : E''} (hc : c ≠ 0) :
(fun _x => c) =O[l] f' ↔ ∃ b, 0 < b ∧ ∀ᶠ x in l, b ≤ ‖f' x‖ :=
by
constructor
· intro h
rcases h.exists_pos with ⟨C, hC₀, hC⟩
refine ⟨‖c‖ / C, div_pos (norm_pos_iff.2 hc) hC₀, ?_⟩
exact hC.bound.mono fun x => (div_le_iff₀' hC₀).2
· rintro ⟨b, hb₀, hb⟩
refine IsBigO.of_bound (‖c‖ / b) (hb.mono fun x hx => ?_)
rw [div_mul_eq_mul_div, mul_div_assoc]
exact le_mul_of_one_le_right (norm_nonneg _) ((one_le_div hb₀).2 hx)
