tendsto_pow_logb_div_mul_add_atTop

English

For a ≠ 0, the quotient (log_b x)^n / (a x + c) tends to 0 as x → ∞.

Русский

Для a ≠ 0 предел (log_b x)^n / (a x + c) при x → ∞ равен 0.

LaTeX

$$$a \neq 0 \Rightarrow \lim_{x \to \infty} \frac{(\log_b x)^n}{a x + c} = 0$$$

Lean4

theorem tendsto_pow_logb_div_mul_add_atTop (a c : ℝ) (n : ℕ) (ha : a ≠ 0) :
    Tendsto (fun x => logb b x ^ n / (a * x + c)) atTop (𝓝 0) := by
  cases eq_or_ne (log b) 0 with
  | inl h => simpa [logb, h] using ((tendsto_mul_add_inv_atTop_nhds_zero _ _ ha).const_mul _)
  | inr h =>
    apply
      (tendsto_pow_log_div_mul_add_atTop (a * (log b) ^ n) (c * (log b) ^ n) n (by positivity)).congr fun x ↦ by
        simp [field, div_pow, logb]

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