English
On the left side of a, for differentiable f and g on Ioo(a,b) with nonzero derivative ratio, L'Hôpital's rule in the derivative form yields the limit of f/g from the left as x approaches a.
Русский
Слева от a, для дифференцируемых f,g на Ioo(a,b) с ненулевым отношением производных, правило Лопиталя через производные даёт предел f/g слева от a.
LaTeX
$$$$ \\text{If } f,g \\text{ differentiable on } Ioo(a,b) \\text{ and } \\lim_{x\\to a^-} \\frac{f'(x)}{g'(x)} = l, \\; \\lim_{x\\to a^-} \\frac{f(x)}{g(x)} = l. $$$$
Lean4
theorem lhopital_zero_left_on_Ioo (hab : a < b) (hdf : DifferentiableOn ℝ f (Ioo a b))
(hg' : ∀ x ∈ Ioo a b, (deriv g) x ≠ 0) (hfb : Tendsto f (𝓝[<] b) (𝓝 0)) (hgb : Tendsto g (𝓝[<] b) (𝓝 0))
(hdiv : Tendsto (fun x => (deriv f) x / (deriv g) x) (𝓝[<] b) l) : Tendsto (fun x => f x / g x) (𝓝[<] b) 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_left_on_Ioo hab (fun x hx => (hdf x hx).hasDerivAt) (fun x hx => (hdg x hx).hasDerivAt) hg'
hfb hgb hdiv
