Theorem 9.41 — equality of mixed partial derivatives

Proved

Rudin.ch09_mixed_partials

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

analysiscalculus

Let $f$ be defined on an open $E \subseteq \mathbb{R}^2$ , suppose $D_1f$ , $D_2f$ and $D_{21}f = D_2(D_1f)$ exist at every point of $E$ , and suppose $D_{21}f$ is continuous at $(a,b) \in E$ . Then $D_{12}f$ exists at $(a,b)$ and $D_{12}f(a,b) = D_{21}f(a,b)$ .

Preamble

import Mathlib

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 9.41: if `D₁f`, `D₂f` and `D₂₁f = D₂(D₁f)` exist on an open set `E ⊆ ℝ²`
and `D₂₁f` is continuous at `(a, b) ∈ E`, then `D₁₂f` exists at `(a, b)` and equals
`D₂₁f (a, b)`. -/
theorem ch09_mixed_partials (E : Set (ℝ × ℝ)) (hE : IsOpen E) (f D1f D2f D21f : ℝ → ℝ → ℝ)
    (h1 : ∀ p ∈ E, HasDerivAt (fun u : ℝ => f u p.2) (D1f p.1 p.2) p.1)
    (h2 : ∀ p ∈ E, HasDerivAt (fun v : ℝ => f p.1 v) (D2f p.1 p.2) p.2)
    (h21 : ∀ p ∈ E, HasDerivAt (fun v : ℝ => D1f p.1 v) (D21f p.1 p.2) p.2)
    (a b : ℝ) (hab : (a, b) ∈ E)
    (hcont : ContinuousAt (fun p : ℝ × ℝ => D21f p.1 p.2) (a, b)) :
    HasDerivAt (fun u : ℝ => D2f u b) (D21f a b) a := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 9, p. 235, Theorems 9.40 and 9.41

Read-back

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

Let $E \subseteq \mathbb{R}\times\mathbb{R}$ be open and let $f, D_1f, D_2f, D_{21}f : \mathbb{R}\to\mathbb{R}\to\mathbb{R}$ be functions of two real arguments. Assume, for every point $p = (p_1,p_2) \in E$ :

the map $u \mapsto f(u, p_2)$ is differentiable at $u = p_1$ with derivative $D_1f(p_1,p_2)$ ;
the map $v \mapsto f(p_1, v)$ is differentiable at $v = p_2$ with derivative $D_2f(p_1,p_2)$ ;
the map $v \mapsto D_1f(p_1, v)$ is differentiable at $v = p_2$ with derivative $D_{21}f(p_1,p_2)$ .

Let $(a,b) \in E$ and assume the function $(u,v) \mapsto D_{21}f(u,v)$ is continuous at $(a,b)$ (as a function on $\mathbb{R}^2$ ).

Then the map $u \mapsto D_2f(u,b)$ is differentiable at $u = a$ , with derivative exactly $D_{21}f(a,b)$ .

So the other mixed partial exists at the single point $(a,b)$ and agrees with the given one there; nothing is asserted at other points, and $D_1f$ , $D_2f$ , $D_{21}f$ are supplied as data satisfying the derivative identities on $E$ rather than being defined by an operator.

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