L'Hôpital's rule

L'Hôpital's rule for the indeterminate form $0/0$.

Suppose $f$ and $g$ are differentiable near $a$, that $g' \neq 0$ near $a$, and that $f(x) \to 0$ and $g(x) \to 0$ as $x \to a$. If $f'/g'$ has a limit $l$ at $a$, then

The rule turns an indeterminate quotient into a quotient of derivatives, which is often tractable. The direction matters: a limit for $f'/g'$ gives one for $f/g$, but not conversely — $f/g$ can converge while $f'/g'$ oscillates. The limit $l$ is taken in an arbitrary filter, so the statement covers $l = \pm\infty$ as well as finite limits. The conclusion is stated on the punctured neighbourhood $\mathring{\mathcal{N}}(a)$ because nothing is assumed about $f(a)$ or $g(a)$ themselves; indeed $g(a) = 0$ is expected.

The rule appeared in de l'Hôpital's Analyse des Infiniment Petits (1696), the first textbook of differential calculus, but is due to Johann Bernoulli, who had contracted to send his discoveries to l'Hôpital in exchange for a salary.

Formalization note. ∀ᶠ x in 𝓝 a means "for all $x$ in some neighbourhood of $a$", and deriv is the total derivative, which is junk-valued (zero) where $f$ is not differentiable — hence the explicit DifferentiableAt hypothesis, without which the statement is false. The result is Mathlib's deriv.lhopital_zero_nhds.