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.
The total (Fréchet) derivative as the linear first-order approximation with remainder
Definition
Let be open, let , and let . The map is totally differentiable at when there is a linear map (A linear map in Euclidean coordinates) such that
where the quotient is considered for with . The map , when it exists, is denoted and called the total derivative. Equivalently, with .
Depends on
- A linear map $L:\mathbb{R}^m\to\mathbb{R}^n$ in Euclidean coordinates
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
- Vector-valued functions $f : A \to \mathbb{R}^m$, their limits and continuity, with the dictionary to the metric notions
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
Used by
- A locally constant step map on the disconnected open set ℝ∖{0} has zero total derivative but is not globally Lipschitz Counterexample
- Continuously differentiable maps, local inverses, and local diffeomorphisms Definition
- The total derivative at a point is unique Lemma
- Dimension, openness, norm, Jacobian, and the native Euclidean linear-map agreement seam Remark
- A total derivative computes every directional derivative, and its matrix is the Jacobian Theorem
- If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative Theorem
- On a convex open set, a uniform bound ‖Df(z)v‖₂≤ M‖v‖₂ implies ‖f(y)-f(x)‖₂≤ M‖y-x‖₂ Theorem
- Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives Theorem
- The chain rule for total derivatives: D(g∘ f)(a)=Dg(f(a))∘ Df(a) Theorem
- The Euclidean implicit function theorem with derivative formula Theorem
- The Euclidean inverse function theorem Theorem
- Total differentiability gives a local O(‖h‖₂) increment bound and therefore continuity Theorem
- Young's theorem: total differentiability of the first partials forces equality of mixed partials Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 110 results over 19 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)