L'Hôpital's Rule

Statement

Let $f$ and $g$ be differentiable near $a$ with $g'(x) \neq 0$ near $a$. If the limit $\lim_{x \to a} \frac{f(x)}{g(x)}$ is an indeterminate form $\frac{0}{0}$ or $\frac{\infty}{\infty}$, and the limit $L = \lim_{x \to a} \frac{f'(x)}{g'(x)}$ exists (or is $\pm\infty$), then:

The rule also applies when $a = \pm\infty$.

Visualization

Recipe for indeterminate forms:

Form	Strategy	Example	Result
$\frac{0}{0}$	Apply L'Hôpital directly	$\lim_{x\to 0}\frac{\sin x}{x}$	$\frac{\cos 0}{1} = 1$
$\frac{\infty}{\infty}$	Apply L'Hôpital directly	$\lim_{x\to\infty}\frac{\ln x}{x}$	$\frac{1/x}{1} \to 0$
$0 \cdot \infty$	Rewrite as $\frac{0}{1/\infty}$	$\lim_{x\to 0^+} x \ln x$	$\frac{\ln x}{1/x} \to 0$
$\infty - \infty$	Common denominator first	$\lim_{x\to 0}(\csc x - \cot x)$	$\to 0$
$1^\infty,\; 0^0,\; \infty^0$	Take $\ln$, reduce to $0/0$	$\lim_{x\to 0^+} x^x$	$e^0 = 1$

Worked example: $\displaystyle\lim_{x \to 0} \frac{1 - \cos x}{x^2}$

Step	Expression	Value
Direct substitution	$\frac{1-\cos 0}{0^2} = \frac{0}{0}$	indeterminate
L'Hôpital once	$\frac{\sin x}{2x}$ at $x=0$	$\frac{0}{0}$ again
L'Hôpital twice	$\frac{\cos x}{2}$ at $x=0$	$\boxed{1/2}$

Proof Sketch

The $0/0$ case at $a$ from the right uses Cauchy's Mean Value Theorem (a generalized MVT):

1. Extend $f, g$ continuously: Set $f(a) = g(a) = 0$.
2. Apply Cauchy MVT on $[a, x]$: For each $x$ near $a$, there exists $c_x \in (a, x)$ with $\frac{f(x)}{g(x)} = \frac{f(x) - f(a)}{g(x) - g(a)} = \frac{f'(c_x)}{g'(c_x)}$.
3. Squeeze: As $x \to a^+$, $c_x$ is sandwiched between $a$ and $x$, so $c_x \to a$.
4. Conclude: $\lim_{x \to a^+} \frac{f(x)}{g(x)} = \lim_{c_x \to a} \frac{f'(c_x)}{g'(c_x)} = L$.

Step 2 relies on the Mean Value TheoremMean Value Theorem$$\exists\, c \in (a,b)\;:\; f'(c) = \frac{f(b)-f(a)}{b-a}$$There exists a point where the instantaneous rate of change equals the average rate of changeRead more →; step 3 uses the Intermediate Value TheoremIntermediate Value Theorem$$f(a) \le y \le f(b) \Rightarrow \exists\, c \in [a,b]:\; f(c) = y$$A continuous function on a closed interval hits every value between its endpointsRead more → to trap $c_x$.

Connections

• Mean Value TheoremMean Value Theorem$$\exists\, c \in (a,b)\;:\; f'(c) = \frac{f(b)-f(a)}{b-a}$$There exists a point where the instantaneous rate of change equals the average rate of changeRead more → — Cauchy's MVT (the engine of L'Hôpital) is a direct generalisation of MVT
• Intermediate Value TheoremIntermediate Value Theorem$$f(a) \le y \le f(b) \Rightarrow \exists\, c \in [a,b]:\; f(c) = y$$A continuous function on a closed interval hits every value between its endpointsRead more → — used to squeeze $c_x \to a$ in the proof
• Chain RuleChain Rule$$\frac{d}{dx}[f(g(x))] = f'(g(x)) \cdot g'(x)$$Differentiate composite functions by peeling layersRead more → — many L'Hôpital computations require differentiating composite functions
• Taylor's TheoremTaylor's Theorem$$f(x) = \sum_{k=0}^{n} \frac{f^{(k)}(x_0)}{k!}(x-x_0)^k + R_n(x)$$Approximate smooth functions by polynomials with explicit error boundsRead more → — Taylor expansions give an alternative shortcut for $0/0$ limits at $0$
• Fundamental Theorem of CalculusFundamental Theorem of Calculus$$\int_a^b f'(x)\,dx = f(b) - f(a)$$Integration and differentiation are inverse operationsRead more → — FTC evaluations often produce $0/0$ forms that L'Hôpital resolves

import Mathlib.Analysis.Calculus.LHopital

open Filter Set

/-- L'Hôpital's rule for the 0/0 form from the right on an open interval (a, b).
    Wraps Mathlib's `HasDerivAt.lhopital_zero_right_on_Ioo`. -/
theorem lhopital_zero_right {f g f' g' : ℝ → ℝ} {a b : ℝ} {l : Filter ℝ}
    (hab : a < b)
    (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x)
    (hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x)
    (hg' : ∀ x ∈ Ioo a b, g' x ≠ 0)
    (hfa : Filter.Tendsto f (nhdsWithin a (Ioi a)) (nhds 0))
    (hga : Filter.Tendsto g (nhdsWithin a (Ioi a)) (nhds 0))
    (hdiv : Filter.Tendsto (fun x => f' x / g' x) (nhdsWithin a (Ioi a)) l) :
    Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Ioi a)) l :=
  HasDerivAt.lhopital_zero_right_on_Ioo hab hff' hgg' hg' hfa hga hdiv