L'Hôpital's rule

Statement

Let $I$ be an open interval and let $c \in I$. Let $f, g$ be real functions differentiable on $I \setminus \{c\}$, with $g'(x) \ne 0$ for all $x \in I \setminus \{c\}$. Assume that $f(x) \to 0$ and $g(x) \to 0$ as $x \to c$, and that $f'(x)/g'(x) \to L$ as $x \to c$. Then $f(x)/g(x) \to L$ as $x \to c$.

Remarks

The proof uses the Cauchy mean value theorem on intervals between $c$ and $x$. Similar forms hold for the indeterminate form $\infty/\infty$, for one-sided limits, and for $x \to \pm\infty$. For example, $\lim_{x \to 0} \frac{1 - \cos x}{x^2} = \lim_{x \to 0} \frac{\sin x}{2x} = \frac{1}{2}$. Mathlib states a form as deriv.lhopital_zero_nhds.

History

Johann Bernoulli found the rule and sent it to Guillaume de l'Hôpital in a letter of 1694. L'Hôpital published it in his textbook of 1696.

Explanations

L1 human

Near $c$, both $f$ and $g$ are close to their tangent lines through $(c, 0)$. So their ratio is close to the ratio of their slopes.