isBigO — Mathlib

English

If eventually ||f|| ≤ ||g|| and g = O_l k, then f = O_l k.

Русский

Если собыфтуально верно, что ||f|| ≤ ||g||, и g = O_l k, то f = O_l k.

LaTeX

$$$(\forall^\! x \in l, \|f(x)\| \le \|g(x)\|) \land (g =O[l] k) \Rightarrow f =O[l] k$$$

Lean4

/-- See also `Asymptotics.IsBigO.of_norm_eventuallyLE`, which is the same lemma
stated using `Filter.EventuallyLE` instead of `Filter.Eventually`. -/
theorem _root_.Filter.Eventually.isBigO {f : α → E} {g : α → ℝ} {l : Filter α} (hfg : ∀ᶠ x in l, ‖f x‖ ≤ g x) :
    f =O[l] g :=
  .of_norm_eventuallyLE hfg

Похожие утверждения