isBigO_sub — Mathlib

English

If HasDerivAtFilter f f' x L holds and f' ≠ 0, then (f x' - f x) = O_L (x' - x) or equivalently (x' - x) = O_L (f x' - f x).

Русский

Если существует HasDerivAtFilter, а производная не ноль, то при этом (f x' - f x) находится в O_L относительно (x' - x).

LaTeX

$$$\\mathrm{HasDerivAtFilter}(f,f',x,L) \\land f' \\neq 0 \\Rightarrow (f x' - f x) =O_L (x' - x).$$$

Lean4

theorem isBigO_sub (h : HasDerivAtFilter f f' x L) : (fun x' => f x' - f x) =O[L] fun x' => x' - x :=
  HasFDerivAtFilter.isBigO_sub h

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