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 be open and let . Suppose every partial derivative exists on a neighbourhood of and is continuous at . Then is totally differentiable at , and is the linear map with matrix .
Facts & Assumptions
Given: The stated neighbourhood existence and continuity hypotheses for all vector partial derivatives.
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).
The vector mean-value inequality says on a real interval when the derivative norm is bounded by (The mean value inequality: if is continuous and differentiable on with , then ).
Proof
Choose a ball around on which the partial derivatives exist. Given , continuity at gives a smaller ball on which every .
For 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 ; its derivative norm is at most .
Summing the segment bounds gives . Since is arbitrary, the normalized remainder tends to zero and is .
Depends on
- Small coordinate-by-coordinate increments stay inside a Euclidean ball and telescope the total increment
- Directional derivatives and partial derivatives of a map $U\subseteq\mathbb{R}^m\to\mathbb{R}^n$
- The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case
- The total (Fréchet) derivative $Df(a)$ as the linear first-order approximation with $o(\|h\|_2)$ remainder
- The mean value inequality: if $f : [a,b] \to \mathbb{R}^m$ is continuous and differentiable on $(a,b)$ with $\lVert f'\rVert_2 \le M$, then $\lVert f(b)-f(a)\rVert_2 \le M(b-a)$
- A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions
- Cauchy-Schwarz $\lvert\langle x,y\rangle\rvert \le \lVert x\rVert_2\lVert y\rVert_2$ with its equality case, the triangle inequality for $\lVert\cdot\rVert_2$, the parallelogram law and polarisation
Used by
- The real complex-squaring map is locally but not globally invertible off the origin Counterexample
- 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
- Repeated derivatives along a line expand by the multinomial formula Lemma
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
- J. Lebl, Basic Analysis I, §8.4 (standard reference, not scraped)