Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedSession-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.

If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative

Statement

Let URmU\subseteq\mathbb R^m be open and let f:URnf:U\to\mathbb R^n. Suppose every partial derivative jf\partial_jf exists on a neighbourhood of aUa\in U and is continuous at aa. Then ff is totally differentiable at aa, and Df(a)Df(a) is the linear map with matrix Jf(a)Jf(a).

Facts & Assumptions

Given: The stated neighbourhood existence and continuity hypotheses for all vector partial derivatives.

[L1]

Coordinate-by-coordinate increments stay inside a Euclidean ball and telescope the total increment (Small coordinate-by-coordinate increments stay inside a Euclidean ball and telescope the total increment).

[L2]

The vector mean-value inequality says f(b)f(a)2M(ba)\lVert f(b)-f(a)\rVert_2\le M(b-a) on a real interval when the derivative norm is bounded by MM (The mean value inequality: if f:[a,b]Rmf : [a,b] \to \mathbb{R}^m is continuous and differentiable on (a,b)(a,b) with f2M\lVert f'\rVert_2 \le M, then f(b)f(a)2M(ba)\lVert f(b)-f(a)\rVert_2 \le M(b-a)).

Proof

technique · direct
1.1

Choose a ball around aa on which the partial derivatives exist. Given ε>0\varepsilon>0, continuity at aa gives a smaller ball on which every jf(z)jf(a)2<ε/m\|\partial_jf(z)-\partial_jf(a)\|_2<\varepsilon/m.

L1L2
2.1

For hh in that smaller ball, [L1] writes the increment as coordinate segments. On each segment apply [L2] to the one-variable map obtained after subtracting the fixed linear term Jf(a)Jf(a); its derivative norm is at most ε/m\varepsilon/m.

step 1.1L2algebra
3.1

Summing the segment bounds gives f(a+h)f(a)Jf(a)h2(ε/m)jhjεh2/mεh2\|f(a+h)-f(a)-Jf(a)h\|_2\le(\varepsilon/m)\sum_j|h_j|\le\varepsilon\|h\|_2/\sqrt m\le\varepsilon\|h\|_2. Since ε\varepsilon is arbitrary, the normalized remainder tends to zero and Jf(a)Jf(a) is Df(a)Df(a).

step 1.1step 2.1L3

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 150 results over 30 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