English
If b ≠ 0, then x^n/(b e^x + c) → 0 as x → ∞.
Русский
Если b ≠ 0, то x^n/(b e^x + c) → 0 при x → ∞.
LaTeX
$$$\\lim_{x \\to +\\infty} \\frac{x^{n}}{b e^{x} + c} = 0 \\quad (b \\neq 0).$$$
Lean4
/-- The function `(x ^ n) / (b * exp x + c)` tends to `0` at `+∞`, for any natural number
`n` and any real numbers `b` and `c` such that `b` is nonzero. -/
theorem tendsto_div_pow_mul_exp_add_atTop (b c : ℝ) (n : ℕ) (hb : 0 ≠ b) :
Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0) :=
by
have H : ∀ d e, 0 < d → Tendsto (fun x : ℝ => x ^ n / (d * exp x + e)) atTop (𝓝 0) :=
by
intro b' c' h
convert (tendsto_mul_exp_add_div_pow_atTop b' c' n h).inv_tendsto_atTop using 1
ext x
simp
rcases lt_or_gt_of_ne hb with h | h
· exact H b c h
· convert (H (-b) (-c) (neg_pos.mpr h)).neg using 1
· ext x
field_simp
rw [← neg_add (b * exp x) c, div_neg, neg_neg]
· rw [neg_zero]
