English
For every s > 0 and any r, log^r x is little-o of x^s as x → ∞.
Русский
Для любого s > 0 и любого r, (лог x)^r = o(x^s) при x → ∞.
LaTeX
$$$\forall s>0\,\forall r\in\mathbb{R}, \; \lim_{x\to\infty} \frac{(\log x)^r}{x^s}=0$$$
Lean4
theorem isLittleO_log_rpow_rpow_atTop {s : ℝ} (r : ℝ) (hs : 0 < s) : (fun x => log x ^ r) =o[atTop] fun x => x ^ s :=
let r' := max r 1
have hr : 0 < r' := lt_max_iff.2 <| Or.inr one_pos
have H : 0 < s / r' := div_pos hs hr
calc
(fun x => log x ^ r) =O[atTop] fun x => log x ^ r' :=
.of_norm_eventuallyLE <|
by
filter_upwards [tendsto_log_atTop.eventually_ge_atTop 1] with x hx
rw [Real.norm_of_nonneg (by positivity)]
gcongr
exacts [hx, le_max_left _ _]
_ =o[atTop] fun x => (x ^ (s / r')) ^ r' :=
((isLittleO_log_rpow_atTop H).rpow hr <| (_root_.tendsto_rpow_atTop H).eventually <| eventually_ge_atTop 0)
_ =ᶠ[atTop] fun x => x ^ s :=
(eventually_ge_atTop 0).mono fun x hx ↦ by simp only [← rpow_mul hx, div_mul_cancel₀ _ hr.ne']
