isBigO_sub — Mathlib

English

From HasGradientAtFilter, the difference f(x')-f(x) is Big-O of x'-x with respect to the norm and inner product with gradient.

Русский

Разность f(x')-f(x) растёт не быстрее чем линейная часть, заданная градиентом.

LaTeX

$$$\\text{HasGradientAtFilter } f f' x L \\Rightarrow (f x' - f x) =O[L] (x' - x)$$$

Lean4

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

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