English
Let ε(x) = 1 / log x for x > 1. Then ε(x) → 0 as x → ∞, hence for every real c < 1, 1 − ε(x) exceeds c eventually; in particular, 1 − ε(x) remains positive for large x. Moreover, ε is differentiable on (1, ∞) with derivative ε'(x) = −1/(x (log x)^2).
Русский
Пусть ε(x) = 1 / log x при x > 1. Тогда ε(x) → 0 при x → ∞, следовательно для каждого c < 1 верно, что 1 − ε(x) будет больше c для больших x; в частности, 1 − ε(x) остается положительной для больших x. Кроме того, ε дифференцируема на (1, ∞) и ε'(x) = −1/(x (log x)^2).
LaTeX
$$$$\varepsilon(x) = \frac{1}{\log x},\quad x>1,$$ \\ $\displaystyle \lim_{x\to\infty} \varepsilon(x) = 0$ and $$\exists X>1\;\forall x\ge X:\; 0<1-\varepsilon(x),$$ \\ and $$\varepsilon'(x) = -\frac{1}{x(\log x)^2},\quad x>1.$$$$
Lean4
theorem eventually_one_sub_smoothingFn_gt_const_real (c : ℝ) (hc : c < 1) : ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x :=
by
have h₁ : Tendsto (fun x => 1 - ε x) atTop (𝓝 1) :=
by
rw [← isEquivalent_const_iff_tendsto one_ne_zero]
exact isEquivalent_one_sub_smoothingFn_one
rw [tendsto_order] at h₁
exact h₁.1 c hc
