isBigO_sub — Mathlib

English

If f is differentiable at x with derivative f', then the map (u,v) ↦ f(u) − f(v) is of first-order smallness in the difference u − v near (x, x); i.e., (f(u) − f(v)) = O(‖u − v‖) as (u, v) → (x, x).

Русский

Если функция f имеет производную в точке x равную f', то разность f(u) − f(v) ведёт себя как сначала‑порядковая малая величина по разности u − v при (u, v) → (x, x); то есть (f(u) − f(v)) = O(‖u − v‖) по мере приближения (u, v) к (x, x).

LaTeX

$$$ (f(u) - f(v)) = O( \\|u - v\\| ) \\quad \\text{as } (u,v) \\to (x,x). $$$

Lean4

theorem isBigO_sub (hf : HasStrictFDerivAt f f' x) :
    (fun p : E × E => f p.1 - f p.2) =O[𝓝 (x, x)] fun p : E × E => p.1 - p.2 :=
  hf.isLittleO.isBigO.congr_of_sub.2 (f'.isBigO_comp _ _)

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