English
Let f,g: R → R be differentiable eventually on (−∞) with g' ≠ 0 eventually, and lim_{x→−∞} f(x) = lim_{x→−∞} g(x) = 0. If the derivative ratio f'(x)/g'(x) tends to some limit l as x → −∞, then the quotient f(x)/g(x) tends to l as x → −∞.
Русский
Пусть f,g: R → R удовлетворяют условиям Лопиталя на минус бесконечности: f(x) → 0, g(x) → 0 при x → −∞, а производные g′ не обращаются в 0 позднее, и отношение производных стремится к l; тогда f/g стремится к l при x → −∞.
LaTeX
$$$$\forall l \in \mathbb{R}, \quad \Big(\forall^{\infty}_{x \to -\infty} \ \text{DifferentiableAt } f x\Big) \land \Big(\forall^{\infty}_{x \to -\infty} \ (\text{deriv } g x) \neq 0\Big) \land \Big(\lim_{x\to -\infty} f(x) = 0\Big) \land \Big(\lim_{x\to -\infty} g(x) = 0\Big) \land \\ \quad \text{Tendsto} (\lambda x. (\text{deriv } f x)/(\text{deriv } g x)) atBot l \Longrightarrow \text{Tendsto} (\lambda x. f(x)/g(x)) atBot l.$$$$
Lean4
/-- **L'Hôpital's rule** for approaching -∞, `deriv` version -/
theorem lhopital_zero_atBot (hdf : ∀ᶠ x : ℝ in atBot, DifferentiableAt ℝ f x) (hg' : ∀ᶠ x : ℝ in atBot, 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 hdg : ∀ᶠ x in atBot, DifferentiableAt ℝ g x :=
hg'.mono fun _ hg' => by_contradiction fun h => hg' (deriv_zero_of_not_differentiableAt h)
have hdf' : ∀ᶠ x in atBot, HasDerivAt f (deriv f x) x := hdf.mono fun _ => DifferentiableAt.hasDerivAt
have hdg' : ∀ᶠ x in atBot, HasDerivAt g (deriv g x) x := hdg.mono fun _ => DifferentiableAt.hasDerivAt
exact HasDerivAt.lhopital_zero_atBot hdf' hdg' hg' hfbot hgbot hdiv
