English
Let a real a and consider the right end behavior as x → +∞. If f and g satisfy a derivative ratio limit along the way and both tend to 0 at +∞, then f/g tends to the same limit as the ratio of derivatives as x → +∞.
Русский
Пусть a — константа; при стремлении x к +∞ условие Лопиталь выполняется: если отношение производных стремится к l и f,g стремятся к 0, то f/g стремится к l.
LaTeX
$$$$ \\text{If } \\lim_{x\\to +\\infty} \\frac{f'(x)}{g'(x)} = l \\text{ and } \\lim_{x\\to +\\infty} f(x) = \\lim_{x\\to +\\infty} g(x) = 0, \\text{ then } \\lim_{x\\to +\\infty} \\frac{f(x)}{g(x)} = l. $$$$
Lean4
theorem lhopital_zero_atBot_on_Iio (hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x)
(hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x) (hg' : ∀ x ∈ Iio a, g' x ≠ 0) (hfbot : Tendsto f atBot (𝓝 0))
(hgbot : Tendsto g atBot (𝓝 0)) (hdiv : Tendsto (fun x => f' x / g' x) atBot l) :
Tendsto (fun x => f x / g x) atBot l := by
-- Here, we essentially compose by `Neg.neg`. The following is mostly technical details.
have hdnf : ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x := fun x hx =>
comp x (hff' (-x) hx) (hasDerivAt_neg x)
have hdng : ∀ x ∈ -Iio a, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x := fun x hx =>
comp x (hgg' (-x) hx) (hasDerivAt_neg x)
rw [neg_Iio] at hdnf
rw [neg_Iio] at hdng
have :=
lhopital_zero_atTop_on_Ioi hdnf hdng
(by
intro x hx h
apply hg' _ (by rw [← neg_Iio] at hx; exact hx)
rwa [mul_comm, ← neg_eq_neg_one_mul, neg_eq_zero] at h)
(hfbot.comp tendsto_neg_atTop_atBot) (hgbot.comp tendsto_neg_atTop_atBot)
(by
simp only [mul_one, mul_neg, neg_div_neg_eq]
exact (hdiv.comp tendsto_neg_atTop_atBot))
have := this.comp tendsto_neg_atBot_atTop
unfold Function.comp at this
simpa only [neg_neg]
