deriv_smoothingFn — Mathlib

English

The derivative of the smoothing function ε is little-o of 1/x as x → ∞: ε'(x) = o(1/x).

Русский

Производная сглаживающей функции ε имеет отношение ε'(x) = o(1/x) при x → ∞.

LaTeX

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

Lean4

theorem deriv_smoothingFn {x : ℝ} (hx : 1 < x) : deriv ε x = -x⁻¹ / (log x ^ 2) :=
  by
  have : log x ≠ 0 := Real.log_ne_zero_of_pos_of_ne_one (by positivity) (ne_of_gt hx)
  change deriv (fun z => 1 / log z) x = -x⁻¹ / (log x ^ 2)
  rw [deriv_fun_div] <;> aesop

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