English
L'Hôpital's rule in the deriv version on the right of a real a with differentiable f and g on Ioo(a,b). If the derivative of g is nonzero and the usual hypotheses hold, then the quotient tends to the limit given by the derivative ratio.
Русский
Правило Лопиталя в версии через производные справа от a для гладких функций на Ioo(a,b). При не нулевой производной g' и выполнении условий, предел f/g равен пределу f'/g'.
LaTeX
$$$$ \\text{If } f,g \\text{ differentiable on } Ioo(a,b), \\ g'(x) \\neq 0, \\; \\lim_{x\\to a^+} \\frac{f'(x)}{g'(x)} = l, \\; \\lim_{x\\to a^+} f(x)=0, \\; \\lim_{x\\to a^+} g(x)=0 \\Rightarrow \\lim_{x\\to a^+} \\frac{f(x)}{g(x)} = l. $$$$
Lean4
theorem lhopital_zero_right_on_Ioo (hab : a < b) (hdf : DifferentiableOn ℝ f (Ioo a b))
(hg' : ∀ x ∈ Ioo a b, 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 hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x := fun x hx => (hdf x hx).differentiableAt (Ioo_mem_nhds hx.1 hx.2)
have hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x := fun x hx =>
by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)
exact
HasDerivAt.lhopital_zero_right_on_Ioo hab (fun x hx => (hdf x hx).hasDerivAt) (fun x hx => (hdg x hx).hasDerivAt)
hg' hfa hga hdiv
