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.
The chain rule for total derivatives:
Statement
Let be totally differentiable at and let be totally differentiable at . Then is totally differentiable at and
Facts & Assumptions
Given: The total first-order expansions of at and at .
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).
Total differentiability gives a local increment bound and therefore continuity (Total differentiability gives a local increment bound and therefore continuity).
Proof
Write and , with both normalized remainders tending to zero.
By [L2], ; boundedness of and the two remainder limits show both and are , including the case .
Substitution into the two expansions leaves , and the composite of linear maps is linear.
Depends on
- The total (Fréchet) derivative $Df(a)$ as the linear first-order approximation with $o(\|h\|_2)$ remainder
- Total differentiability gives a local $O(\|h\|_2)$ increment bound and therefore continuity
- Every Euclidean linear map has a unique matrix and satisfies $\|Lh\|_2\le K\|h\|_2$ for some $K\ge0$
- A linear map $L:\mathbb{R}^m\to\mathbb{R}^n$ in Euclidean coordinates
Used by
- Newton maps are uniform contractions near a point with invertible derivative Lemma
- Repeated derivatives along a line expand by the multinomial formula Lemma
- A constrained local extremum annihilates every velocity of a differentiable parametrization Theorem
- Change of variables for an injective C¹ map on a compact Jordan set Theorem
- On a convex open set, a uniform bound ‖Df(z)v‖₂≤ M‖v‖₂ implies ‖f(y)-f(x)‖₂≤ M‖y-x‖₂ Theorem
- The Euclidean implicit function theorem with derivative formula Theorem
- The Euclidean inverse function theorem Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 69 results over 18 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)