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 удовлетворяют условиям Лопиталя на бесконечности: для x → +∞ выполняются f(x) → 0, g(x) → 0, существует f', g' такие, что f′(x)/g′(x) tends к l, и g′(x) ≠ 0 позднее. Тогда f(x)/g(x) tends к 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)) atTop l \Longrightarrow \text{Tendsto} (\lambda x. f(x)/g(x)) atTop l.$$$$
Lean4
/-- **L'Hôpital's rule** for approaching +∞, `deriv` version -/
theorem lhopital_zero_atTop (hdf : ∀ᶠ x : ℝ in atTop, DifferentiableAt ℝ f x) (hg' : ∀ᶠ x : ℝ in atTop, deriv g x ≠ 0)
(hftop : Tendsto f atTop (𝓝 0)) (hgtop : Tendsto g atTop (𝓝 0))
(hdiv : Tendsto (fun x => (deriv f) x / (deriv g) x) atTop l) : Tendsto (fun x => f x / g x) atTop l :=
by
have hdg : ∀ᶠ x in atTop, DifferentiableAt ℝ g x :=
hg'.mp (Eventually.of_forall fun _ hg' => by_contradiction fun h => hg' (deriv_zero_of_not_differentiableAt h))
have hdf' : ∀ᶠ x in atTop, HasDerivAt f (deriv f x) x := hdf.mono fun _ => DifferentiableAt.hasDerivAt
have hdg' : ∀ᶠ x in atTop, HasDerivAt g (deriv g x) x := hdg.mono fun _ => DifferentiableAt.hasDerivAt
exact HasDerivAt.lhopital_zero_atTop hdf' hdg' hg' hftop hgtop hdiv
