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.

A total derivative computes every directional derivative, and its matrix is the Jacobian

Statement

If $f : U \to R^{n}$ is totally differentiable at $a$ , then $D_{v} f (a)$ exists for every $v \in R^{m}$ and equals $D f (a) v$ . In particular $\partial_{j} f (a) = D f (a) e_{j}$ , and the matrix of $D f (a)$ is $J f (a)$ .

Facts & Assumptions

Given: A total derivative $D f (a)$ and a direction $v \in R^{m}$ .

[L1]

The total-derivative definition supplies the normwise remainder estimate for every $ε > 0$ ; in positive source dimension this is equivalently the normalized remainder tending to zero as $h$ tends to zero (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

[L2]

The directional derivative is the derivative of $t \mapsto f (a + t v)$ at zero, and partial derivatives use standard-basis directions (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ).

Proof

technique · direct

1.1givenL1L2algebra

If $n = 0$ , the line map has only the zero value, so its directional derivative is the zero vector by the zero-target case of [L2], and this is $D f (a) v$ . Every column identity then has zero rows. The case of a zero-dimensional source has only $v = 0$ and no partial directions; it is covered by the zero-direction argument below. For the remaining nonzero-direction argument assume $n \geq 1$ .

1.2L1L2algebra

If $v = 0$ , then $(f (a + t v) - f (a)) / t = 0 = D f (a) 0$ for every $t \neq 0$ , so [L2] gives $D_{0} f (a) = D f (a) 0$ . For the remaining case assume $v \neq 0$ . For sufficiently small $t \neq 0$ , openness of $U$ gives $a + t v \in U$ and $t v \neq 0$ . Write $f (a + t v) - f (a) = t D f (a) v + r (t v)$ , where $∥ r (t v) ∥_{2} / ∥ t v ∥_{2} \to 0$ by [L1].

2.1step 1.2L2algebra

Dividing by $t$ gives $(f (a + t v) - f (a)) / t = D f (a) v + r (t v) / t$ , and $∥ r (t v) / t ∥_{2} = ∥ v ∥_{2} ∥ r (t v) ∥_{2} / ∥ t v ∥_{2} \to 0$ ; hence [L2] yields $D_{v} f (a) = D f (a) v$ .

3.1step 1.2step 2.1∎

Taking $v = e_{j}$ identifies the $j$ th column of the matrix of $D f (a)$ with the vector of $j$ th partial derivatives, which is precisely the Jacobian.

Depends on

Used by

…and 17 more results.

Dependency tree · two levels

14 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.3 (standard reference, not scraped)