English
Let a real a and consider the behavior as x → +∞. If f,g are differentiable with derivative ratio tending to l and f,g → 0 at +∞, then f/g → l at +∞.
Русский
Пусть a есть некоторое число; при x → +∞, если f,g дифференцируемы, и отношение производных стремится к l, а f,g стремятся к 0, то f/g стремится к l при x → +∞.
LaTeX
$$$$ \\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_atTop_on_Ioi (hdf : DifferentiableOn ℝ f (Ioi a)) (hg' : ∀ x ∈ Ioi a, (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 hdf : ∀ x ∈ Ioi a, DifferentiableAt ℝ f x := fun x hx => (hdf x hx).differentiableAt (Ioi_mem_nhds hx)
have hdg : ∀ x ∈ Ioi a, DifferentiableAt ℝ g x := fun x hx =>
by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)
exact
HasDerivAt.lhopital_zero_atTop_on_Ioi (fun x hx => (hdf x hx).hasDerivAt) (fun x hx => (hdg x hx).hasDerivAt) hg'
hftop hgtop hdiv
