English
For x → +∞, the derivative version of L'Hôpital yields the quotient limit if derivative ratios converge and f,g vanish at infinity.
Русский
Для x → +∞, производная версия Лопиталя даёт предел отношения, если отношение производных сходится, а f,g стремятся к нулю на бесконечности.
LaTeX
$$$$ \\lim_{x\\to +\\infty} \\frac{f(x)}{g(x)} = l \\quad \\text{under } \\lim_{x\\to +\\infty} \\frac{f'(x)}{g'(x)} = l, \\; \\lim f = \\lim g = 0. $$$$
Lean4
/-- L'Hôpital's rule for approaching a real from the right, `HasDerivAt` version -/
theorem lhopital_zero_nhdsGT (hff' : ∀ᶠ x in 𝓝[>] a, HasDerivAt f (f' x) x)
(hgg' : ∀ᶠ x in 𝓝[>] a, HasDerivAt g (g' x) x) (hg' : ∀ᶠ x in 𝓝[>] a, g' x ≠ 0) (hfa : Tendsto f (𝓝[>] a) (𝓝 0))
(hga : Tendsto g (𝓝[>] a) (𝓝 0)) (hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l) :
Tendsto (fun x => f x / g x) (𝓝[>] a) l :=
by
rw [eventually_iff_exists_mem] at *
rcases hff' with ⟨s₁, hs₁, hff'⟩
rcases hgg' with ⟨s₂, hs₂, hgg'⟩
rcases hg' with ⟨s₃, hs₃, hg'⟩
let s := s₁ ∩ s₂ ∩ s₃
have hs : s ∈ 𝓝[>] a := inter_mem (inter_mem hs₁ hs₂) hs₃
rw [mem_nhdsGT_iff_exists_Ioo_subset] at hs
rcases hs with ⟨u, hau, hu⟩
refine lhopital_zero_right_on_Ioo hau ?_ ?_ ?_ hfa hga hdiv <;> intro x hx <;> apply_assumption <;>
first
| exact (hu hx).1.1
| exact (hu hx).1.2
| exact (hu hx).2
