English
A more symmetric variant of IsBigO bound with a reciprocal constant: f =O[l] g iff there exists c > 0 with c ||f|| ≤ ||g|| eventually.
Русский
Еще одна симметричная форма границы Big-O: f =O[l] g тогда и только тогда, когда существует c > 0, такое что c||f|| ≤ ||g|| неотклоняемо вдоль l.
LaTeX
$$$ f =O[l] g \iff \exists c > 0, \forall^\! x \in l, c\|f(x)\| ≤ \|g(x)\|$$$
Lean4
/-- Definition of `IsBigO` in terms of filters, with a positive constant. -/
theorem isBigO_iff' {g : α → E'''} : f =O[l] g ↔ ∃ c > 0, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ :=
by
refine ⟨fun h => ?mp, fun h => ?mpr⟩
case mp =>
rw [isBigO_iff] at h
obtain ⟨c, hc⟩ := h
refine ⟨max c 1, zero_lt_one.trans_le (le_max_right _ _), ?_⟩
filter_upwards [hc] with x hx
apply hx.trans
gcongr
exact le_max_left _ _
case mpr =>
rw [isBigO_iff]
obtain ⟨c, ⟨_, hc⟩⟩ := h
exact ⟨c, hc⟩
