Cauchy's Mean Value Theorem

Statement

Let $f, g : \mathbb{R} \to \mathbb{R}$ both be continuous on $[a, b]$ and differentiable on $(a, b)$. Then there exists $c \in (a, b)$ such that

When $g'(c) \neq 0$ and $g(b) \neq g(a)$ this rearranges to

The ordinary Mean Value Theorem is the special case $g(x) = x$.

Visualization

Take $f(x) = x^2$ and $g(x) = x^3$ on $[1, 2]$.

Values:

quantity	value
$f(1) = 1$, $f(2) = 4$	$f(2)-f(1) = 3$
$g(1) = 1$, $g(2) = 8$	$g(2)-g(1) = 7$
ratio $\frac{f(b)-f(a)}{g(b)-g(a)}$	$\frac{3}{7}$

Derivatives: $f'(x) = 2x$, $g'(x) = 3x^2$.

We need $\frac{f'(c)}{g'(c)} = \frac{2c}{3c^2} = \frac{2}{3c} = \frac{3}{7}$, so:

$x$	$f'(x)$	$g'(x)$	ratio $f'/g'$
1.0	2.0	3.0	0.667
1.556	3.111	7.259	0.429 = 3/7 ✓
2.0	4.0	12.0	0.333

Proof Sketch

1. Auxiliary function: Define $h(x) = (g(b) - g(a)) f(x) - (f(b) - f(a)) g(x)$.
2. Equal endpoints: $h(a) = (g(b)-g(a))f(a) - (f(b)-f(a))g(a)$ and $h(b) = (g(b)-g(a))f(b) - (f(b)-f(a))g(b)$; direct algebra shows $h(a) = h(b)$.
3. Apply Rolle's Theorem: $h$ is continuous on $[a,b]$, differentiable on $(a,b)$, and $h(a) = h(b)$, so there exists $c \in (a,b)$ with $h'(c) = 0$.
4. Expand: $h'(c) = (g(b)-g(a)) f'(c) - (f(b)-f(a)) g'(c) = 0$ is exactly the conclusion.

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 reduces to the standard MVT when $g(x) = x$
• L'Hôpital's RuleL'Hôpital's Rule$$\lim_{x \to a} \frac{f(x)}{g(x)} = \lim_{x \to a} \frac{f'(x)}{g'(x)}$$Evaluate indeterminate-form limits by differentiating numerator and denominatorRead more → — L’Hôpital's rule for $0/0$ indeterminate forms is proved using Cauchy's MVT
• 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 → — higher-order Taylor remainder estimates use iterated applications of Cauchy's MVT
• Rolle's TheoremRolle's Theorem$$f(a)=f(b)\implies\exists\,c\in(a,b):\;f'(c)=0$$Between two equal values of a differentiable function there exists a point with zero derivativeRead more → — the proof constructs an auxiliary function and applies Rolle directly

Alternative name: the ratio form $\frac{f(b)-f(a)}{g(b)-g(a)} = \frac{f'(c)}{g'(c)}$ (when $g(b) \neq g(a)$ and $g' \neq 0$) is also called the Generalized Mean Value Theorem; it is a direct rearrangement of the multiplicative statement above.

import Mathlib.Analysis.Calculus.Deriv.MeanValue

/-- Cauchy's Mean Value Theorem: wraps `exists_ratio_hasDerivAt_eq_ratio_slope`. -/
theorem cauchy_mvt {f g f' g' : ℝ → ℝ} {a b : ℝ} (hab : a < b)
    (hfc : ContinuousOn f (Set.Icc a b))
    (hgc : ContinuousOn g (Set.Icc a b))
    (hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x)
    (hgg' : ∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) :
    ∃ c ∈ Set.Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c :=
  exists_ratio_hasDerivAt_eq_ratio_slope f f' hab hfc hff' g g' hgc hgg'