Differentiability from partial derivatives continuous at a point

Proved

Rudin.ch09_differentiable_of_continuous_partials

by ;ptE}w2NFf · Sep 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscalculusdifferential-calculus

Let $E \subseteq \mathbb{R}^n$ be an open set and let $\mathbf{f} : \mathbb{R}^n \to \mathbb{R}^m$ . Suppose that for each coordinate direction $j$ the partial derivative

(D_j \mathbf{f})(\mathbf{y}) \;=\; \lim_{t \to 0} \frac{\mathbf{f}(\mathbf{y} + t\mathbf{e}_j) - \mathbf{f}(\mathbf{y})}{t}

exists at every point $\mathbf{y} \in E$ , where $\mathbf{e}_j$ denotes the $j$ -th standard basis vector of $\mathbb{R}^n$ . Fix a point $\mathbf{x} \in E$ and assume in addition that each of the $n$ maps $\mathbf{y} \mapsto (D_j \mathbf{f})(\mathbf{y})$ is continuous at $\mathbf{x}$ . Then $\mathbf{f}$ is differentiable at $\mathbf{x}$ , and its differential is the linear map

\mathbf{f}'(\mathbf{x})\mathbf{v} \;=\; \sum_{j=1}^{n} v_j \, (D_j \mathbf{f})(\mathbf{x}), \qquad \mathbf{v} = (v_1, \dots, v_n).

Two features of the hypotheses deserve emphasis. Existence of the partial derivatives is required throughout the open set $E$ , whereas their continuity is required only at the single point $\mathbf{x}$ . Mere existence of the partial derivatives at a point does not imply differentiability there, so the continuity hypothesis is what upgrades the $n$ one-dimensional derivatives to a genuine differential.

This is the analytic content of the sufficiency half of Rudin's Theorem 9.21. It is stated pointwise so that it can be applied at each point of an open set: combined with the continuity of $\mathbf{x} \mapsto \mathbf{f}'(\mathbf{x})$ , which follows from continuity of the partial derivatives, it yields the equivalence between $\mathbf{f}$ being continuously differentiable on $E$ and all of its partial derivatives existing and being continuous on $E$ .

Formalization Note The domain and codomain are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). The $j$ -th partial derivative is written as a one-dimensional derivative at $t = 0$ of the restriction $t \mapsto \mathbf{f}(\mathbf{y} + t\mathbf{e}_j)$ , with $\mathbf{e}_j$ given by EuclideanSpace.single j 1. The differential is assembled as $\sum_j \pi_j(\cdot)\,(D_j\mathbf{f})(\mathbf{x})$ , where $\pi_j$ is the $j$ -th coordinate projection; ContinuousLinearMap.smulRight combines the scalar functional $\pi_j$ with the vector $(D_j\mathbf{f})(\mathbf{x})$ into a continuous linear map.

Preamble

import Mathlib

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Chapter 9, Theorem 9.21 (pointwise core of the sufficiency direction): if the
coordinate partial derivatives of `f` exist throughout an open set `E` and are continuous at
a point `x ∈ E`, then `f` is differentiable at `x`, with differential sending `v` to
`∑ j, v j • D j x`. -/
theorem ch09_differentiable_of_continuous_partials
    (n m : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) (hE : IsOpen E)
    (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m))
    (D : Fin n → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m))
    (hD : ∀ j : Fin n, ∀ y ∈ E,
      HasDerivAt (fun t : ℝ => f (y + t • EuclideanSpace.single j (1 : ℝ))) (D j y) 0)
    (x : EuclideanSpace ℝ (Fin n)) (hx : x ∈ E)
    (hc : ∀ j : Fin n, ContinuousAt (D j) x) :
    HasFDerivAt f
      (∑ j : Fin n, (EuclideanSpace.proj j : EuclideanSpace ℝ (Fin n) →L[ℝ] ℝ).smulRight
        (D j x)) x := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 9, p. 219, Theorem 9.21 (sufficiency direction; the pointwise differentiability step established in its proof)

View graph