isLittleO_deriv_one_add_smoothingFn

English

The derivative of 1 + ε x is o(1/x) as x → ∞.

Русский

Производная 1 + ε(x) как функция от x есть o(1/x) при x → ∞.

LaTeX

$$$$\frac{d}{dx}(1+\varepsilon(x)) = o\left(\frac{1}{x}\right)\quad (x\to\infty).$$$$

Lean4

theorem isLittleO_deriv_one_add_smoothingFn : deriv (fun x => 1 + ε x) =o[atTop] fun (x : ℝ) => x⁻¹ :=
  calc
    deriv (fun x => 1 + ε x)
    _ =ᶠ[atTop] fun z => deriv ε z := by filter_upwards [eventually_gt_atTop 1] with x hx; rw [deriv_fun_add] <;> aesop
    _ =o[atTop] fun x => x⁻¹ := isLittleO_deriv_smoothingFn

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