English
Assume a real a and take the left-infinite border; under L'Hôpital-type hypotheses, the quotient limit follows from the derivative ratio as x → −∞.
Русский
Пусть a real; при x → −∞ выполняются аналогичные условия Лопиталя: предел отношения f(x)/g(x) соответствует пределy отношения производных.
LaTeX
$$$$ \\text{If } \\lim_{x\\to -\\infty} \\frac{f'(x)}{g'(x)} = l, \\lim_{x\\to -\\infty} f(x) = \\lim_{x\\to -\\infty} g(x) = 0 \\Rightarrow \\lim_{x\\to -\\infty} \\frac{f(x)}{g(x)} = l. $$$$
Lean4
theorem lhopital_zero_atBot_on_Iio (hdf : DifferentiableOn ℝ f (Iio a)) (hg' : ∀ x ∈ Iio a, (deriv g) x ≠ 0)
(hfbot : Tendsto f atBot (𝓝 0)) (hgbot : Tendsto g atBot (𝓝 0))
(hdiv : Tendsto (fun x => (deriv f) x / (deriv g) x) atBot l) : Tendsto (fun x => f x / g x) atBot l :=
by
have hdf : ∀ x ∈ Iio a, DifferentiableAt ℝ f x := fun x hx => (hdf x hx).differentiableAt (Iio_mem_nhds hx)
have hdg : ∀ x ∈ Iio a, DifferentiableAt ℝ g x := fun x hx =>
by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)
exact
HasDerivAt.lhopital_zero_atBot_on_Iio (fun x hx => (hdf x hx).hasDerivAt) (fun x hx => (hdg x hx).hasDerivAt) hg'
hfbot hgbot hdiv
