Alphabeta MathHow 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.
A total derivative computes every directional derivative, and its matrix is the Jacobian
Statement
If is totally differentiable at , then exists for every and equals . In particular , and the matrix of is .
Facts & Assumptions
Given: A total derivative and a direction .
In the total-derivative definition, the normalized remainder tends to zero as tends to zero (The total (Fréchet) derivative as the linear first-order approximation with remainder).
The directional derivative is the derivative of at zero, and partial derivatives use standard-basis directions (Directional derivatives and partial derivatives of a map ).
Proof
For , write , where by [L1].
Dividing by gives , and ; hence [L2] yields .
Taking identifies the th column of the matrix of with the vector of th partial derivatives, which is precisely the Jacobian.
Depends on
- The total (Fréchet) derivative $Df(a)$ as the linear first-order approximation with $o(\|h\|_2)$ remainder
- 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
- Every Euclidean linear map has a unique matrix and satisfies $\|Lh\|_2\le K\|h\|_2$ for some $K\ge0$
Used by
- x²y/(x²+y²) has every directional derivative at the origin but is not totally differentiable there Counterexample
- The Jacobian determinant of a square-dimensional C¹ map is the determinant of its Jacobian matrix Definition
- For a differentiable scalar field, Dᵥf(a)=⟨∇ f(a),v⟩ and the unit direction of steepest ascent is the normalized gradient Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 85 results over 21 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.3 (standard reference, not scraped)