TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Young's theorem: total differentiability of the first partials forces equality of mixed partials

Statement

Let $f$ be defined on a disk $U$ about $(a, b)$ , with $f_{x}$ and $f_{y}$ existing on $U$ . If $f_{x}$ and $f_{y}$ are totally differentiable at $(a, b)$ , then both mixed partials exist there and $f_{x y} (a, b) = f_{y x} (a, b)$ .

Facts & Assumptions

Given: The hypotheses of the statement.

[L1]

Total differentiability supplies a linear approximation with an error that is little-oh of the Euclidean increment (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

[L2]

A total derivative is linear. Restricting its defining expansion to a coordinate axis shows directly that its corresponding coordinate coefficient is the partial derivative in that coordinate (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

[L3]

The one-variable mean-value theorem applies to a continuous restriction differentiable in the open interval; differentiability supplies the needed continuity (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ , A function differentiable at $c$ is continuous at $c$ ).

Proof

technique · direct

1.1

By [L1] and [L2], write $D f_{x} (a, b) (s, t) = A s + B t$ and $D f_{y} (a, b) (s, t) = C s + D t$ .

L1L2givenalgebra

$f_{x} (a + s, b + t) = f_{x} (a, b) + A s + B t + o ⁣ (\sqrt{s^{2} + t^{2}})$

and analogously $f_{y} (a + s, b + t) = f_{y} (a, b) + C s + D t + o ⁣ (\sqrt{s^{2} + t^{2}})$ . Restricting the first expansion to $s = 0$ and the second to $t = 0$ shows that $B = f_{x y} (a, b)$ and $C = f_{y x} (a, b)$ ; in particular both mixed partials exist.

2.1

By [L3], for small nonzero $h$ , define the following rectangular difference.

step 1.1L3algebrachoose

$Δ_{h} : = f (a + h, b + h) - f (a + h, b) - f (a, b + h) + f (a, b) .$

Apply the mean-value theorem to $x \mapsto f (x, b + h) - f (x, b)$ on the interval with endpoints $a, a + h$ . For some $θ_{h}$ between $0$ and $1$ ,

$Δ_{h} = h (f_{x} (a + θ_{h} h, b + h) - f_{x} (a + θ_{h} h, b)) = B h^{2} + o (h^{2}),$

where the last equality is the first expansion of step 1.1 at $(θ_{h} h, h)$ and $(θ_{h} h, 0)$ .

2.2

Apply [L3] instead to $y \mapsto f (a + h, y) - f (a, y)$ on the interval with endpoints $b, b + h$ .

step 1.1L3algebrachoose

For some $η_{h}$ between $0$ and $1$ ,

$Δ_{h} = h (f_{y} (a + h, b + η_{h} h) - f_{y} (a, b + η_{h} h)) = C h^{2} + o (h^{2}),$

by the second expansion of step 1.1 at $(h, η_{h} h)$ and $(0, η_{h} h)$ .

3.1

Steps 2.1 and 2.2 give $(B - C) h^{2} = o (h^{2})$ . Divide by $h^{2}$ and let $h \to 0$ to obtain $B = C$ , hence $f_{x y} (a, b) = f_{y x} (a, b)$ .

step 1.1step 2.1step 2.2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Mixed partial derivatives (Eremenko) (standard reference, not scraped)