eventually_one_sub_smoothingFn_pos

English

For every x > 1, the function 1 − ε(x) is differentiable at x and its derivative is 1/(x (log x)^2).

Русский

Для каждого x > 1 функция 1 − ε(x) дифференцируема в точке x и ее производная равна 1/(x (log x)^2).

LaTeX

$$$$x>1 \implies \frac{d}{dx}\left(1-\varepsilon(x)\right) = \frac{1}{x(\log x)^2}.$$$$

Lean4

theorem eventually_one_sub_smoothingFn_pos : ∀ᶠ (n : ℕ) in atTop, 0 < 1 - ε n :=
  (eventually_one_sub_smoothingFn_pos_real).natCast_atTop

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