English
A concrete positive constant version of IsBigO_iff'': there exists c = 2 such that c ||f|| ≤ ||g|| eventually if and only if f =O[l] g.
Русский
Конкретная версия IsBigO_iff'' с константой c = 2: найдется c = 2 такое, что c ||f|| ≤ ||g|| неотклоняемо вдоль l тогда и только тогда f =O[l] g.
LaTeX
$$$ f =O[l] g \iff \exists c = 2 > 0, \forall^\! x \in l, 2 \|f(x)\| ≤ \|g(x)\| $$$
Lean4
/-- Definition of `IsBigO` in terms of filters, with the constant in the lower bound. -/
theorem isBigO_iff'' {g : α → E'''} : f =O[l] g ↔ ∃ c > 0, ∀ᶠ x in l, c * ‖f x‖ ≤ ‖g x‖ :=
by
refine ⟨fun h => ?mp, fun h => ?mpr⟩
case mp =>
rw [isBigO_iff'] at h
obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
filter_upwards [hc] with x hx
rwa [inv_mul_le_iff₀ (by positivity)]
case mpr =>
rw [isBigO_iff']
obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
filter_upwards [hc] with x hx
rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx
