isLittleO_abs_log_rpow_rpow_nhdsGT_zero

English

Let s < 0. For every r ∈ ℝ, as x → 0^+ we have |log x|^r = o(x^s); equivalently, lim_{x→0^+} |log x|^r / x^s = 0.

Русский

Пусть s < 0. Для любого r ∈ ℝ при x → 0^+ выполняется |log x|^r = o(x^s); эквивалентно lim_{x→0^+} |log x|^r / x^s = 0.

LaTeX

$$$$ \forall r \in \mathbb{R},\ \forall s<0:\quad |\log x|^{r} = o\left(x^{s}\right) \ \text{as } x \to 0^{+}. $$$$

Lean4

theorem isLittleO_abs_log_rpow_rpow_nhdsGT_zero {s : ℝ} (r : ℝ) (hs : s < 0) :
    (fun x => |log x| ^ r) =o[𝓝[>] 0] fun x => x ^ s :=
  ((isLittleO_log_rpow_rpow_atTop r (neg_pos.2 hs)).comp_tendsto tendsto_inv_nhdsGT_zero).congr'
    (mem_of_superset (Icc_mem_nhdsGT one_pos) fun x hx => by simp [abs_of_nonpos, log_nonpos hx.1 hx.2])
    (eventually_mem_nhdsWithin.mono fun x hx => by
      rw [Function.comp_apply, inv_rpow hx.out.le, rpow_neg hx.out.le, inv_inv])

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