isBigO_sub_rev — Mathlib

English

The reverse Big-O relation holds: (x' - x) = O_L (f x' - f x) if HasDerivAtFilter f f' x L with f' ≠ 0.

Русский

Обратная связь Big-O: (x' - x) = O_L (f x' - f x) при наличии HasDerivAtFilter c f' x L с f' ≠ 0.

LaTeX

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

Lean4

nonrec theorem isBigO_sub_rev (hf : HasDerivAtFilter f f' x L) (hf' : f' ≠ 0) :
    (fun x' => x' - x) =O[L] fun x' => f x' - f x :=
  suffices AntilipschitzWith ‖f'‖₊⁻¹ (smulRight (1 : 𝕜 →L[𝕜] 𝕜) f') from hf.isBigO_sub_rev this
  AddMonoidHomClass.antilipschitz_of_bound (smulRight (1 : 𝕜 →L[𝕜] 𝕜) f') fun x => by
    simp [norm_smul, ← div_eq_inv_mul, mul_div_cancel_right₀ _ (mt norm_eq_zero.1 hf')]

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