isBigO_sub_rev — Mathlib

English

A strong Frechet derivative implies a reversed big-O bound for the difference quotient in two coordinates.

Русский

Строгая производная Фреше порождает обратное отношение big-O для разности двух координат.

LaTeX

$$HasStrictFDerivAt f f' x → Asymptotics.IsBigO (nhds { fst := x, snd := x }) (fun p => f p.fst - f p.snd) (fun p => p.fst - p.snd)$$

Lean4

theorem isBigO_sub_rev {f' : E ≃L[𝕜] F} (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) x) :
    (fun p : E × E => p.1 - p.2) =O[𝓝 (x, x)] fun p : E × E => f p.1 - f p.2 :=
  ((f'.isBigO_comp_rev _ _).trans (hf.isLittleO.trans_isBigO (f'.isBigO_comp_rev _ _)).right_isBigO_add).congr
    (fun _ => rfl) fun _ => sub_add_cancel _ _

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