isLittleO_pow_logb_id_atTop — Mathlib

English

For any natural n, (log_b x)^n = o(x) as x → ∞.

Русский

Для любого натурального n, (log_b x)^n = o(x) при x → ∞.

LaTeX

$$$\forall n,\ (\log_b x)^n = o[\mathrm{atTop}]\, x$$$

Lean4

theorem isLittleO_pow_logb_id_atTop {n : ℕ} : (fun x => logb b x ^ n) =o[atTop] id :=
  by
  rw [Asymptotics.isLittleO_iff_tendsto']
  · simpa using tendsto_pow_logb_div_mul_add_atTop 1 0 n one_ne_zero
  · filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim

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