eventually_one_sub_smoothingFn_pos_real

English

For x > 1, the function ε(x) = 1/log x is differentiable, and hence 1 − ε(x) and 1 + ε(x) are differentiable as well; in particular, the derivative of ε is −1/(x (log x)^2).

Русский

Для x > 1 функция ε(x) = 1/log x дифференцируема; следовательно, 1 − ε(x) и 1 + ε(x) тоже дифференцируемы; производная ε равна −1/(x (log x)^2).

LaTeX

$$$$x>1 \implies \varepsilon \text{ differentiable at } x, \quad \varepsilon'(x) = -\frac{1}{x(\log x)^2}.$$$$

Lean4

theorem eventually_one_sub_smoothingFn_pos_real : ∀ᶠ (x : ℝ) in atTop, 0 < 1 - ε x :=
  eventually_one_sub_smoothingFn_gt_const_real 0 zero_lt_one

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