TheoremStatement: AI-adaptedProof: AI-generated

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 $U \subseteq R^{m}$ be open and let $f : U \to R^{n}$ . Suppose every partial derivative $\partial_{j} f$ exists on a neighbourhood of $a \in U$ and is continuous at $a$ . Then $f$ is totally differentiable at $a$ , and $D f (a)$ is the linear map with matrix $J f (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) ∥_{2} \leq M (b - a)$ on a real interval when the derivative norm is bounded by $M$ (The mean value inequality: if $f : [a, b] \to R^{m}$ is continuous and differentiable on $(a, b)$ with $∥ f^{'} ∥_{2} \leq M$ , then $∥ f (b) - f (a) ∥_{2} \leq M (b - a)$ ).

[L3]

Cauchy--Schwarz gives $\sum_{j < m} ∣ h_{j} ∣ \leq \sqrt{m} ∥ h ∥_{2}$ (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[L4]

The space $R^{0}$ is the zero space, its standard basis is empty, and its Euclidean norm is zero (The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ clause 5, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). Coordinate matrices represent linear maps by their finite coordinate sums, including empty rows or columns.

[L5]

A Euclidean linear map preserves real linear combinations in all finite dimensions (A linear map $L : R^{m} \to R^{n}$ in Euclidean coordinates). Total differentiability is the normwise epsilon-delta remainder estimate, including its explicit zero-dimensional cases (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

Proof

technique · direct

1.1givenL4L5algebra

If $m = 0$ , then $a = 0$ , $U = {0}$ , and the only increment is $h = 0$ . The unique linear map $L : R^{0} \to R^{n}$ has $L 0 = 0$ , so $f (a + h) - f (a) - L h = 0$ for every admissible increment. It satisfies the normwise remainder estimate with any $δ > 0$ . There are no coordinate directions; $J f (a)$ is the empty-column $n \times 0$ matrix of $L$ . Thus the conclusion holds without dividing by $m$ or invoking a punctured limit at an isolated point.

1.2givenL4L5algebra

If $m \geq 1$ and $n = 0$ , every value of $f$ is the unique zero vector. The unique linear map $L : R^{m} \to R^{0}$ therefore leaves zero remainder for every increment, and its matrix, like $J f (a)$ , has zero rows. This proves the conclusion directly, without applying the positive-codomain vector mean-value inequality. For the rest of the proof assume $m, n \geq 1$ .

1.3givenL1L2

Choose a ball around $a$ on which the partial derivatives exist. Given $ε > 0$ , continuity at $a$ gives a smaller ball on which every $∥ \partial_{j} f (z) - \partial_{j} f (a) ∥_{2} < ε / m$ .

2.1step 1.3L2algebra

For $h$ 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 $J f (a)$ ; its derivative norm is at most $ε / m$ .

3.1step 1.1step 1.2step 1.3step 2.1L3L5∎

Summing the segment bounds gives $∥ f (a + h) - f (a) - J f (a) h ∥_{2} \leq (ε / m) \sum_{j} ∣ h_{j} ∣ \leq ε ∥ h ∥_{2} / \sqrt{m} \leq ε ∥ h ∥_{2}$ . Since $ε$ is arbitrary, this verifies the normwise remainder condition and $J f (a)$ is $D f (a)$ . Together with the two zero-dimensional cases this proves the full Statement.

Depends on

Used by

The finite-basis projector energy model supplies a C1 Hermitian response map Corollary
Time reversal of the homogeneous wave equation Corollary
A critical value can have a smooth level set Counterexample
An isolated boundary point obstructs pointwise-zero Green data Counterexample
The cone x²+y²=z² has a rank drop at its apex Counterexample
The cusp y²=x³ has a rank drop at the origin Counterexample
The real complex-squaring map is locally but not globally invertible off the origin Counterexample
Cᵏ Euclidean maps and diffeomorphisms Definition
Poisson kernel from a Dirichlet Green function Definition
Wave equation, Cauchy data and wave speed Definition
A Euclidean sphere is a regular level set with tangent hyperplanes Example
A positive-definite quadratic ellipsoid is a regular level set Example
A radial three-dimensional wave reduces to one dimension Example
Brownian finite-dimensional density Example
Newton shell theorem from harmonic mean values Example
Newtonian potential of radial compact data Example
Right- and left-travelling waves Example
The map (x,y)↦(x,xy) has nonconstant rank on every neighbourhood of the origin Example
The natural Neumann condition from a free endpoint in one dimension Example
The one-sheeted hyperboloid is a regular surface of revolution Example
The orthogonal group is a regular level set of dimension n(n-1)/2 Example
The polynomial map (x,y)↦(1+x+2y+x², 2x+3y+xy) and its Jacobian Example
The unit circle is locally a C¹ graph at every point Example
Two constraints on a sphere-plane circle, where one multiplier solution is only a local maximum Example
FALSE: a critical value must have a singular level set False statement
FALSE: an everywhere-invertible derivative gives a global inverse False statement
FALSE: every injective real-differentiable planar map has nonzero Jacobian False statement
FALSE: every level set of a smooth map is locally a graph False statement
A C¹ map sends a compact set of content zero to a set of content zero Lemma
A C² saddle function has C¹ Morse coordinates Lemma
A local Sobolev chain rule for C¹ postcomposition Lemma
A transport equation restricts to a linear ODE along each characteristic Lemma
A vector field along an ODE solution has an explicit derivative bound Lemma
A vector line integral along an image arc is the parameter line integral of the pulled-back field Lemma
Differentiating an integral with moving endpoints Lemma
Differentiation of an integral functional under growth domination Lemma
Factorisation of the one-dimensional wave operator Lemma
Forward-difference Jacobian error bound Lemma
General solution of the one-dimensional wave equation Lemma
Invertible linear substitutions preserve Schwartz space Lemma

…and 54 more results.

Dependency tree · two levels

68 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

J. Lebl, Basic Analysis I, §8.4 (standard reference, not scraped)