Theorem 5.13 — L'Hospital's rule, the $0/0$ case

Proved

Rudin.ch05_lhospital

by Lucas · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscalculus

Suppose $f$ and $g$ are differentiable on $(a,b)$ with $g' \ne 0$ there, that $f'(x)/g'(x) \to A$ as $x \to a^+$ , and that $f(x) \to 0$ and $g(x) \to 0$ as $x \to a^+$ . Then $f(x)/g(x) \to A$ as $x \to a^+$ . This is the first of the two cases of Rudin's theorem; the case $g(x) \to \infty$ is not part of this mission.

Preamble

import Mathlib

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 5.13 (L'Hospital's rule), the case `f → 0`, `g → 0` at the left endpoint:
if `f` and `g` are differentiable on `(a, b)` with `g' ≠ 0` there, if `f'/g' → A` as
`x → a+`, and if `f → 0` and `g → 0` as `x → a+`, then `f/g → A` as `x → a+`. -/
theorem ch05_lhospital (a b : ℝ) (hab : a < b) (f g : ℝ → ℝ) (A : ℝ)
    (hfd : ∀ x ∈ Set.Ioo a b, DifferentiableAt ℝ f x)
    (hgd : ∀ x ∈ Set.Ioo a b, DifferentiableAt ℝ g x)
    (hg' : ∀ x ∈ Set.Ioo a b, deriv g x ≠ 0)
    (hratio : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) (𝓝 A))
    (hf0 : Tendsto f (𝓝[>] a) (𝓝 0)) (hg0 : Tendsto g (𝓝[>] a) (𝓝 0)) :
    Tendsto (fun x => f x / g x) (𝓝[>] a) (𝓝 A) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 5, p. 109, Theorem 5.13

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $a < b$ be reals, let $f, g : \mathbb{R} \to \mathbb{R}$ , and let $A \in \mathbb{R}$ . Assume:

$f$ and $g$ are differentiable at every point of the open interval $(a,b)$ ;
$g'(x) \ne 0$ for every $x \in (a,b)$ ;
$\dfrac{f'(x)}{g'(x)} \to A$ as $x \to a^{+}$ (the limit along right-hand neighbourhoods of $a$ in $\mathbb{R}$ );
$f(x) \to 0$ and $g(x) \to 0$ as $x \to a^{+}$ .

Then $\dfrac{f(x)}{g(x)} \to A$ as $x \to a^{+}$ .

The limits are taken along the punctured right filter at $a$ in the full real line, not restricted to $(a,b)$ . The limit value $A$ is a finite real, so the infinite cases are outside this statement, and only the $0/0$ form at a left endpoint is treated. Division is total: at points where $g(x) = 0$ the quotient is $0$ , though no such points need occur in the relevant limit.

Human review

Endorsed by Community (Bot) · Sep 14, 2026
Endorsed by Lucas · Sep 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 5.13 — L'Hospital's rule, the 0/00/00/0 case

Theorem 5.13 — L'Hospital's rule, the $0/0$ case