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 total (Fréchet) derivative as the linear first-order approximation with remainder
Definition
Let , let be open in the metric induced by its Euclidean norm, let , and let . The map is totally differentiable at when there is a linear map (A linear map in Euclidean coordinates) such that for every there is for which
The map , when it exists, is denoted and called the total derivative. Equivalently, with the displayed remainder estimate for every . At the remainder is zero because .
For , openness of provides admissible nonzero increments arbitrarily near zero, and dividing the estimate by gives the usual notation
where the quotient is considered for with . Conversely this punctured normwise limit gives the estimate above (using a smaller positive tolerance if necessary). Thus the positive-dimensional definition is unchanged. This is the multivariate normwise remainder condition; no limit at an isolated point is asserted.
When , the Euclidean zero space consists only of , so and ; its Euclidean norm and induced metric exist by A norm on a real vector space, the induced metric, and the dictionary with the metric axioms. The unique linear map sends to , and its remainder is identically zero. It is therefore the total derivative by the displayed estimate, with any . When , the unique map and the unique linear map into likewise have zero remainder, in every source dimension.
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
- Backpropagation through a finite shared-parameter recurrence Algorithm
- Finite-budget pseudo-arclength continuation with a certified local corrector Algorithm
- Heavy-ball momentum Algorithm
- Nesterov accelerated gradient Algorithm
- One-step episodic actor–critic with a bootstrapped critic Algorithm
- The subdifferential of a differentiable convex function is its gradient singleton Corollary
- A locally constant step map on the disconnected open set ℝ∖{0} has zero total derivative but is not globally Lipschitz Counterexample
- Minima of viscosity subsolutions need not be subsolutions Counterexample
- Zero derivative need not give constancy on a disconnected open set Counterexample
- Bounded C1 domains and their outward normals Definition
- C¹ critical loci and values for Euclidean maps Definition
- Certified differentiable IVP approximation interface for shooting Definition
- Complement splitting and range projection for a simple fold Definition
- Continuous linearized BVP operator and its conditioning Definition
- Continuously differentiable maps, local inverses, and local diffeomorphisms Definition
- Differentiable stationary stochastic policies and score vectors Definition
- Euclidean hypersurface normals, shape operators and curvature Definition
- Finite parameterized state-step graphs and objectives Definition
- Finite straight-line computational programs and real-arithmetic tapes Definition
- Holomorphic functions on an open subset of ℂᵐ Definition
- Hopf spectral and multilinear normal-form data Definition
- Local periodic-orbit, Poincare-return, and Floquet data Definition
- Orientation-preserving conformality for a real-differentiable complex map at a point Definition
- Piecewise smooth shocks and one-sided traces Definition
- Scalar conservation laws, fluxes and Cauchy data Definition
- The Hamilton--Jacobi Cauchy problem and its classical solutions Definition
- The neural tangent kernel of a differentiable parameterized function Definition
- The Wirtinger derivatives ∂_z f and ∂_z̄f, and antiholomorphic functions Definition
- Viscosity subsolutions and supersolutions of a first-order equation and of the Cauchy problem Definition
- Wirtinger operators in ℂᵐ Definition
- A bootstrapped critic can bias the first actor update Example
- A gradient-descent path can be bounded below when the objective is not Example
- A Hopf--Lax solution with a forming corner from smooth data Example
- A state baseline can eliminate this estimator's variance Example
- Newtonian potential of radial compact data Example
- One-step Bernoulli REINFORCE has the exact expected gradient Example
- r² sin(1/r) is differentiable at the origin with a discontinuous gradient Example
- The polydisc boundary is not a smooth hypersurface, so the Szegő definition does not apply Example
- Vanishing viscosity selects the Hopf--Lax solution for bounded data Example
- xy sin(1/(x²+y²)) is differentiable at the origin with unbounded partial derivatives nearby Example
…and 46 more results.
Dependency tree · two levels
31 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)