tendsto_pow_log_div_mul_add_atTop

English

Let a, b be real numbers with a ≠ 0, and n a natural number. Then the limit as x → ∞ of log(x)^n / (a x + b) is 0; equivalently, log(x)^n grows strictly slower than x.

Русский

Пусть a, b ∈ ℝ, a ≠ 0, и натуральное n. Тогда предел при x → ∞ дроби log(x)^n / (a x + b) равен 0; т.е. log(x)^n растёт медленнее x.

LaTeX

$$$$ \\lim_{x \\to \\infty} \\frac{\\log(x)^n}{a x + b} = 0, \\quad a \\neq 0. $$$$

Lean4

theorem tendsto_pow_log_div_mul_add_atTop (a b : ℝ) (n : ℕ) (ha : a ≠ 0) :
    Tendsto (fun x => log x ^ n / (a * x + b)) atTop (𝓝 0) :=
  ((tendsto_div_pow_mul_exp_add_atTop a b n ha.symm).comp tendsto_log_atTop).congr' <| by
    filter_upwards [eventually_gt_atTop (0 : ℝ)] with x hx using by simp [exp_log hx]

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