English
Given differentiable f and g on Ioo(a,b) with g' ≠ 0, the L'Hôpital rule in derivative form yields the limit of f/g near a from the right.
Русский
Дано дифференцируемые f и g на Ioo(a,b) с g' ≠ 0; правило Лопиталя в форме через производные даёт предел f/g слева от a справа.
LaTeX
$$$$ \\lim_{x\\to a^+} \\frac{f(x)}{g(x)} = l \\text{ if } \\lim_{x\\to a^+} \\frac{f'(x)}{g'(x)} = l. $$$$
Lean4
/-- **L'Hôpital's rule** for approaching a real from the right, `deriv` version -/
theorem lhopital_zero_nhdsGT (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_nhdsGT hdf' hdg' hg' hfa hga hdiv
