isBigOWith_abs_right — Mathlib

English

If g(x) is bounded by C times f(x) at x and g(x) is not too large, then the Big-OWith bound holds when moving from nhdsWithin x s to nhdsWithin x (insert x s).

Русский

Если существует константа C такая, что ||g(x)|| ≤ C ||f(x)|| при x, и g(x) ограничено, то граница IsBigOWith сохраняется при переходе от nhdsWithin x s к nhdsWithin x с вставкой x.

LaTeX

$$$$ \|g(x)\| \le C \|f(x)\| \quad \Rightarrow\quad \IsBigOWith C (nhdsWithin x (insert x s))\; g\; f.$$$$

Lean4

@[simp]
theorem isBigOWith_abs_right : (IsBigOWith c l f fun x => |u x|) ↔ IsBigOWith c l f u :=
  @isBigOWith_norm_right _ _ _ _ _ _ f u l

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