English
A version of L'Hôpital's rule for derivatives: if f and g are differentiable with certain limits, then the ratio f/g tends to the appropriate limit given by the derivatives.
Русский
Версия правила Лопиталя для производных: если f и g дифференцируемы и выполняются некоторые условия, то отношение f/g приближается к пределу, заданному производными.
LaTeX
$$$lhopital\ deriv\ lhopital_zero_nhds$$$
Lean4
/-- **L'Hôpital's rule** for approaching a real, `deriv` version -/
theorem lhopital_zero_nhds (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
apply lhopital_zero_nhdsNE <;>
(first
| apply eventually_nhdsWithin_of_eventually_nhds
| apply tendsto_nhdsWithin_of_tendsto_nhds) <;>
assumption
