English
If f,g are differentiable on Ioo(a,b) with derivative ratio satisfying the needed limit near a from the left, then the left-hand limit of f/g equals the same limit l.
Русский
Если f,g дифференцируемы на Ioo(a,b) и отношение производных удовлетворяет нужному пределу слева от a, то предел слева f/g равен этому пределу l.
LaTeX
$$$$ \\lim_{x\\to a^-} \\frac{f(x)}{g(x)} = l \\text{ under appropriate left-sided derivative bounds.} $$$$
Lean4
/-- **L'Hôpital's rule** for approaching a real from the left, `deriv` version -/
theorem lhopital_zero_nhdsLT (hdf : ∀ᶠ x in 𝓝[<] a, DifferentiableAt ℝ f x) (hg' : ∀ᶠ x in 𝓝[<] a, deriv g x ≠ 0)
(hfa : Tendsto f (𝓝[<] a) (𝓝 0)) (hga : Tendsto g (𝓝[<] a) (𝓝 0))
(hdiv : Tendsto (fun x => (deriv f) x / (deriv g) x) (𝓝[<] a) l) : Tendsto (fun x => f x / g x) (𝓝[<] a) l :=
by
have hdg : ∀ᶠ x in 𝓝[<] a, DifferentiableAt ℝ g x :=
hg'.mono fun _ hg' => by_contradiction fun h => hg' (deriv_zero_of_not_differentiableAt h)
have hdf' : ∀ᶠ x in 𝓝[<] a, HasDerivAt f (deriv f x) x := hdf.mono fun _ => DifferentiableAt.hasDerivAt
have hdg' : ∀ᶠ x in 𝓝[<] a, HasDerivAt g (deriv g x) x := hdg.mono fun _ => DifferentiableAt.hasDerivAt
exact HasDerivAt.lhopital_zero_nhdsLT hdf' hdg' hg' hfa hga hdiv
