TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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_{xy}(a,b)=f_{yx}(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 $Df(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 $Df(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 $Df_x(a,b)(s,t)=As+Bt$ and $Df_y(a,b)(s,t)=Cs+Dt$ .

L1L2givenalgebra

$f_x(a+s,b+t)=f_x(a,b)+As+Bt+o\!\left(\sqrt{s^2+t^2}\right)$

and analogously $f_y(a+s,b+t)=f_y(a,b)+Cs+Dt+o\!\left(\sqrt{s^2+t^2}\right)$ . Restricting the first expansion to $s=0$ and the second to $t=0$ shows that $B=f_{xy}(a,b)$ and $C=f_{yx}(a,b)$ ; in particular both mixed partials exist.

2.1

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

step 1.1L3algebrachoose

$\Delta_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 $\theta_h$ between $0$ and $1$ ,

$\Delta_h=h\bigl(f_x(a+\theta_hh,b+h)-f_x(a+\theta_hh,b)\bigr)=Bh^2+o(h^2),$

where the last equality is the first expansion of step 1.1 at $(\theta_hh,h)$ and $(\theta_hh,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 $\eta_h$ between $0$ and $1$ ,

$\Delta_h=h\bigl(f_y(a+h,b+\eta_hh)-f_y(a,b+\eta_hh)\bigr)=Ch^2+o(h^2),$

by the second expansion of step 1.1 at $(h,\eta_hh)$ and $(0,\eta_hh)$ .

3.1

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

step 1.1step 2.1step 2.2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 58 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

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