isLittleO_log_rpow_nhdsGT_zero — Mathlib

English

Let hr: r < 0. Then log x = o(x^r) as x → 0^+; equivalently, lim_{x→0^+} log x / x^r = 0.

Русский

Пусть r < 0. Тогда log x = o(x^r) при x → 0^+; эквивалентно lim_{x→0^+} log x / x^r = 0.

LaTeX

$$$$ \lim_{x \to 0^{+}} \frac{\log x}{x^{r}} = 0 \quad (r<0). $$$$

Lean4

theorem isLittleO_log_rpow_nhdsGT_zero {r : ℝ} (hr : r < 0) : log =o[𝓝[>] 0] fun x => x ^ r :=
  (isLittleO_abs_log_rpow_rpow_nhdsGT_zero 1 hr).neg_left.congr'
    (mem_of_superset (Icc_mem_nhdsGT one_pos) fun x hx => by simp [abs_of_nonpos (log_nonpos hx.1 hx.2)]) .rfl

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