Theorem 9.19 — mean value inequality on a convex set

Proved

Rudin.ch09_bounded_derivative

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

analysiscalculus

If $\mathbf{f}$ is differentiable on a convex open set $E$ with $\|\mathbf{f}'(\mathbf{x})\| \le M$ for all $\mathbf{x} \in E$ , then $|\mathbf{f}(\mathbf{b}) - \mathbf{f}(\mathbf{a})| \le M|\mathbf{b} - \mathbf{a}|$ for all $\mathbf{a}, \mathbf{b} \in E$ . Taking $M = 0$ shows a map with vanishing derivative on a convex open set is constant.

Preamble

import Mathlib

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 9.19: if `f` is differentiable on a convex open set `E` with
`‖f'(x)‖ ≤ M` there, then `f` is Lipschitz with constant `M` on `E`; in particular a vanishing
derivative on a convex open set forces `f` to be constant. -/
theorem ch09_bounded_derivative (n m : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) (hE : IsOpen E)
    (hconv : Convex ℝ E) (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m))
    (f' : EuclideanSpace ℝ (Fin n) → (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)))
    (hf : ∀ x ∈ E, HasFDerivAt f (f' x) x) (M : ℝ) (hM : ∀ x ∈ E, ‖f' x‖ ≤ M) :
    ∀ a ∈ E, ∀ b ∈ E, ‖f b - f a‖ ≤ M * ‖b - a‖ := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 9, p. 218, Theorem 9.19

Read-back

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

Let $n,m \in \mathbb{N}$ , let $E \subseteq \mathbb{R}^n$ be open and convex, let $f : \mathbb{R}^n\to\mathbb{R}^m$ , and let $f'$ assign to each point a continuous linear map $\mathbb{R}^n \to \mathbb{R}^m$ . Assume that for every $x \in E$ , $f$ has Fréchet derivative $f'(x)$ at $x$ , and that there is a real $M$ with $\lVert f'(x)\rVert \le M$ (operator norm) for every $x \in E$ . Then

\lVert f(b) - f(a) \rVert \;\le\; M\,\lVert b - a \rVert \qquad\text{for all } a, b \in E .

The Lipschitz estimate is asserted only for pairs of points of $E$ . The constant $M$ is not assumed nonnegative in advance (though the hypothesis forces $M \ge 0$ as soon as $E$ is nonempty). The special case $M = 0$ gives $f$ constant on $E$ , but that conclusion is not stated separately.

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